diff options
| author | ebotcazou <ebotcazou@138bc75d-0d04-0410-961f-82ee72b054a4> | 2013-09-18 10:35:53 +0000 |
|---|---|---|
| committer | ebotcazou <ebotcazou@138bc75d-0d04-0410-961f-82ee72b054a4> | 2013-09-18 10:35:53 +0000 |
| commit | 760e8c4ebefc1300c0d6838e9d587022571bd0e5 (patch) | |
| tree | d6f058591c988a59e2b3d0ed02b61558a31ef79e /gcc/ada/gcc-interface/decl.c | |
| parent | fae32d6f1d16ed0f7aebe1b623c46a88c46b439f (diff) | |
| download | ppe42-gcc-760e8c4ebefc1300c0d6838e9d587022571bd0e5.tar.gz ppe42-gcc-760e8c4ebefc1300c0d6838e9d587022571bd0e5.zip | |
* gcc-interface/decl.c (gnat_to_gnu_entity) <E_Abstract_State>: New.
git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@202690 138bc75d-0d04-0410-961f-82ee72b054a4
Diffstat (limited to 'gcc/ada/gcc-interface/decl.c')
| -rw-r--r-- | gcc/ada/gcc-interface/decl.c | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/gcc/ada/gcc-interface/decl.c b/gcc/ada/gcc-interface/decl.c index 26342e2a012..456d7ab7ad9 100644 --- a/gcc/ada/gcc-interface/decl.c +++ b/gcc/ada/gcc-interface/decl.c @@ -4812,6 +4812,12 @@ gnat_to_gnu_entity (Entity_Id gnat_entity, tree gnu_expr, int definition) saved = true; break; + case E_Abstract_State: + /* This is a SPARK annotation that only reaches here when compiling in + ASIS mode and has no characteristics to annotate. */ + gcc_assert (type_annotate_only); + return error_mark_node; + default: gcc_unreachable (); } |
