logic_parser.mly

;

ext_module_markup:
| MODULE ext_identifier COLON { $2 }
;

ext_function_markup:
| FUNCTION ext_identifier COLON { $2, loc() }
;

ext_contract_markup:
| CONTRACT ext_identifier_opt COLON { $2 }
;

stmt_markup:
| any_identifier { $1 }
| CONSTANT10 { $1 }
;

stmt_markup_attr:
| stmt_markup                      { [$1] }
| stmt_markup stmt_markup_attr { $1 :: $2 }
;

ext_at_stmt_markup:
| EXT_AT stmt_markup_attr COLON { $2 }
;

/*** function and statement contracts ***/

spec:
| contract EOF { fst $1 }
;

contract:
| requires terminates decreases simple_clauses behaviors complete_or_disjoint
    { let requires=$1 in
      let (allocation,assigns,post_cond,extended) = $4 in
      let behaviors = $5 in
      let (completes,disjoints) = $6 in
      let behaviors =
        if requires <> [] || post_cond <> [] ||
	   allocation <> FreeAllocAny ||
           assigns <> WritesAny || extended <> []
        then
          (Cabshelper.mk_behavior
             ~requires ~post_cond ~assigns ~allocation ~extended ())
          :: behaviors
        else if $2<>None || $3<>None ||
                behaviors<>[] || completes<>[] ||disjoints<>[]
        then behaviors
        else raise (Not_well_formed (loc(),"Empty annotation is not allowed"))
      in
        { spec_terminates = $2;
          spec_variant = $3;
          spec_behavior = behaviors;
          spec_complete_behaviors = completes;
          spec_disjoint_behaviors = disjoints;
        }, loc()
    }
| requires ne_terminates REQUIRES { clause_order 3 "requires" "terminates" }
| requires terminates ne_decreases REQUIRES
      { clause_order 4 "requires" "decreases" }
| requires terminates ne_decreases TERMINATES
      { clause_order 4 "terminates" "decreases" }
| requires terminates decreases ne_simple_clauses REQUIRES
      { clause_order 5 "requires" "post-condition, assigns or allocates" }
| requires terminates decreases ne_simple_clauses TERMINATES
      { clause_order 5 "terminates" "post-condition, assigns or allocates" }
| requires terminates decreases ne_simple_clauses DECREASES
      { clause_order 5 "decreases" "post-condition, assigns or allocates" }
| requires terminates decreases simple_clauses ne_behaviors TERMINATES
      { clause_order 6 "terminates" "behavior" }
| requires terminates decreases simple_clauses ne_behaviors DECREASES
      { clause_order 6 "decreases" "behavior" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  REQUIRES
      { clause_order 7 "requires" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  TERMINATES
      { clause_order 7 "terminates" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  DECREASES
      { clause_order 7 "decreases" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  BEHAVIOR
      { clause_order 7 "behavior" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  ASSIGNS
      { clause_order 7 "assigns" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  ALLOCATES
      { clause_order 7 "allocates" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  FREES
      { clause_order 7 "frees" "complete or disjoint" }
| requires terminates decreases simple_clauses behaviors ne_complete_or_disjoint
  post_cond_kind
      { clause_order 7 "post-condition" "complete or disjoint" }
;

// use that to detect potentially missing ';' at end of clause
clause_kw:
| CHECK_REQUIRES { "check requires" }
| REQUIRES { "requires" }
| ASSUMES {"assumes"}
| ASSIGNS { "assigns" }
| post_cond { snd $1 }
| DECREASES { "decreases"}
| BEHAVIOR { "behavior"}
| ALLOCATES {"allocates"}
| FREES {"frees"}
| COMPLETE {"complete"}
| DISJOINT {"disjoint"}
/* often, we'll be in c_kw_mode, where these keywords are
   recognized as identifiers... */
| IDENTIFIER { $1 }
| EXT_CONTRACT { $1 }
| EOF { "end of annotation" }
;

requires:
| /* epsilon */ { [] }
| ne_requires { $1 }
;

ne_requires:
| REQUIRES full_lexpr SEMICOLON requires { toplevel_pred false $2::$4 }
| CHECK_REQUIRES full_lexpr SEMICOLON requires { toplevel_pred true $2 :: $4 }
| REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
| CHECK_REQUIRES full_lexpr clause_kw { missing 2 ";" $3 }
;

terminates:
| /* epsilon */              { None }
| ne_terminates { Some $1 }
;

ne_terminates:
| TERMINATES full_lexpr SEMICOLON { $2 }
| TERMINATES full_lexpr clause_kw { missing 2 ";" $3 }
;

decreases:
| /* epsilon */   { None }
| ne_decreases { Some $1 }
;

ne_decreases:
| DECREASES variant SEMICOLON { $2 }
| DECREASES variant clause_kw { missing 2 ";" $3 }
;

variant:
| full_lexpr FOR any_identifier { ($1, Some $3) }
| full_lexpr                    { ($1, None) }
;

simple_clauses:
| /* epsilon */ { FreeAllocAny,WritesAny,[],[] }
| ne_simple_clauses { $1 }
;

allocation:
| ALLOCATES full_zones { FreeAlloc([],$2) }
| FREES full_zones { FreeAlloc($2,[]) }

ne_simple_clauses:
| post_cond_kind full_lexpr SEMICOLON simple_clauses
    { let only_check, kind = $1 in
      let allocation,assigns,post_cond,extended = $4 in
      allocation,assigns,
      ((kind,toplevel_pred only_check $2)::post_cond),extended }
| allocation SEMICOLON simple_clauses
    { let allocation,assigns,post_cond,extended = $3 in
      let a = concat_allocation allocation $1 in
      a,assigns,post_cond,extended
    }
| ASSIGNS full_assigns SEMICOLON simple_clauses
    { let allocation,assigns,post_cond,extended = $4 in
      let a = concat_assigns assigns $2
      in allocation,a,post_cond,extended
    }
| EXT_CONTRACT grammar_extension SEMICOLON simple_clauses
    { let allocation,assigns,post_cond,extended = $4 in
      let processed = Logic_env.preprocess_extension $1 $2 in
      allocation,assigns,post_cond,($1,processed)::extended
    }
| post_cond_kind full_lexpr clause_kw { missing 2 ";" $3 }
| allocation clause_kw { missing 1 ";" $2 }
| ASSIGNS full_assigns clause_kw { missing 2 ";" $3 }
| EXT_CONTRACT grammar_extension clause_kw { missing 1 ";" $3 }
;

grammar_extension:
/* Grammar Extensibility for plugins */
| full_zones { $1 }
;

post_cond_kind:
| post_cond { fst $1 }
;

behaviors:
| /* epsilon */ { [] }
| ne_behaviors { $1 }

ne_behaviors:
| BEHAVIOR behavior_name COLON behavior_body behaviors
      { let (assumes,requires,(allocation,assigns,post_cond,extended)) = $4 in
        let behaviors = $5 in
        let b =
          Cabshelper.mk_behavior
            ~name:$2
            ~assumes ~requires ~post_cond ~assigns ~allocation ~extended ()
        in b::behaviors
      }

behavior_body:
| assumes requires simple_clauses { $1,$2,$3 }
| assumes ne_requires ASSUMES
      { clause_order 3 "assumes" "requires" }
| assumes requires ne_simple_clauses ASSUMES
      { clause_order 4 "assumes" "assigns or post-condition" }
| assumes requires ne_simple_clauses REQUIRES
      { clause_order 4 "requires" "assigns or post-condition" }
;

assumes:
| /* epsilon */ { [] }
| ASSUMES full_lexpr SEMICOLON assumes { $2::$4 }
| ASSUMES full_lexpr clause_kw { missing 2 ";" $3 }
;

complete_or_disjoint:
| /* epsilon */ { [],[] }
| ne_complete_or_disjoint { $1 }

ne_complete_or_disjoint:
| COMPLETE BEHAVIORS behavior_name_list SEMICOLON
    complete_or_disjoint
      { let complete,disjoint = $5 in $3::complete, disjoint }
| DISJOINT BEHAVIORS behavior_name_list SEMICOLON
          complete_or_disjoint
      { let complete,disjoint = $5 in complete,$3::disjoint }
/* complete behaviors decreases; is valid (provided there's a behavior
   named decreases)
*/
| COMPLETE BEHAVIORS ne_behavior_name_list clause_kw { missing 3 ";" $4 }
| DISJOINT BEHAVIORS ne_behavior_name_list clause_kw { missing 3 ";" $4 }
;

/*** assigns and tsets ***/

assigns:
| zones { List.map (fun x -> (x,FromAny)) $1 }
| ne_zones FROM zones {List.map (fun x -> (x, From $3)) $1}
;

zones:
| ne_zones { $1 }
| NOTHING  { [] }
;

ne_zones:
| ne_lexpr_list { $1 }
;

/*** annotations ***/

annot:
| annotation EOF  { $1 }
| is_acsl_spec any EOF { Aspec }
| decl_list EOF   { Adecl ($1) }
| CUSTOM any_identifier COLON custom_tree EOF { Acustom(loc (),$2, $4) }
;

custom_tree:
| TYPE type_spec  { CustomType $2 }
| LOGIC lexpr     { CustomLexpr $2 }
| any_identifier_non_logic  { CustomOther($1,[]) }
| any_identifier_non_logic LPAR custom_tree_list RPAR  { CustomOther($1,$3) }
;

custom_tree_list:
| custom_tree   { [$1] }
| custom_tree COMMA custom_tree_list  { $1::$3 }
;

annotation:
| loop_annotations
      { let (b,v,p) = $1 in
        (* TODO: do better, do not lose the structure ! *)
        let l = b@v@p in
        Aloop_annot (loc (), l) }
| FOR ne_behavior_name_list COLON contract_or_code_annotation
      { $4 $2 }
| pragma_or_code_annotation { Acode_annot (loc(),$1) }
| pragma_or_code_annotation beg_pragma_or_code_annotation
      { raise
          (Not_well_formed (loc(),
                            "Only one code annotation is allowed per comment"))
      }
| full_identifier_or_typename { Aattribute_annot (loc (), $1) }
;

contract_or_code_annotation:
| contract
      { fun bhvs -> let s, pos = $1 in Acode_annot (pos, AStmtSpec (bhvs,s)) }
| code_annotation { fun bhvs -> Acode_annot (loc(), ($1 bhvs)) }
;

/*** loop annotations ***/

loop_annotations:
| loop_annot_stack
    { let (i,fa,a,b,v,p, e) = $1 in
      let invs = List.map (fun i -> AInvariant([],true,i)) i in
      let ext = List.map (fun x -> AExtended([],true, x)) e in
      let oth = match a with
        | WritesAny -> b
        | Writes _ ->
            (* by definition all existing AAssigns are tied to at least
               one behavior. No need to merge against them. *)
            AAssigns ([],a)::b
      in
      let oth = match fa with
        | FreeAllocAny -> oth
        | _ -> AAllocation ([],fa)::oth
      in
	(invs@oth@ext,v,p)
    }
;

/* TODO: gather loop assigns that are related to the same behavior */
loop_annot_stack:
| loop_invariant loop_annot_opt
    { let (i,fa,a,b,v,p,e) = $2 in ($1::i,fa,a,b,v,p,e) }
| loop_effects loop_annot_opt
    { let (i,fa,a,b,v,p,e) = $2 in (i,fa,concat_assigns a $1,b,v,p,e) }
| loop_allocation loop_annot_opt
    { let (i,fa,a,b,v,p,e) = $2 in (i,concat_allocation fa $1,a,b,v,p,e) }
| FOR ne_behavior_name_list COLON loop_annot_stack
    { let (i,fa,a,b,v,p,e) = $4 in
      let behav = $2 in
      let invs = List.map (fun i -> AInvariant(behav,true,i)) i in
      let ext = List.map (fun x -> AExtended(behav,true,x)) e in
      let oth = concat_loop_assigns_allocation b behav a fa in
      ([],FreeAllocAny,WritesAny,invs@ext@oth,v,p,[])
    }
| loop_variant loop_annot_opt
    { let pos,loop_variant = $1 in
      let (i,fa,a,b,v,p,e) = $2 in
      check_empty
        (pos,"loop invariant is not allowed after loop variant.") i ;
      check_empty
        (pos, "loop extension is not allowed after loop variant.") e;
      (match fa with
        | FreeAlloc(f,a) ->
	    check_empty
              (pos,"loop frees is not allowed after loop variant.") f ;
	    check_empty
              (pos,"loop allocates is not allowed after loop variant.") a
        | FreeAllocAny -> ());
      (match a with
          WritesAny -> ()
        | Writes _ ->
          raise
            (Not_well_formed
               (pos,"loop assigns is not allowed after loop variant.")));
      check_empty
        (pos,"loop behavior is not allowed after loop variant.") b ;
      check_empty
        (pos,"loop annotations can have at most one variant.") v ;
      (i,fa,a,b,AVariant loop_variant::v,p,e) }
| loop_pragma loop_annot_opt
    { let (i,fa,a,b,v,p,e) = $2 in (i,fa,a,b,v,APragma (Loop_pragma $1)::p,e) }
| loop_grammar_extension loop_annot_opt {
    let (i,fa,a,b,v,p,e) = $2 in
    (i,fa,a,b,v,p, $1::e)
  }
;

loop_annot_opt:
| /* epsilon */
    { ([], FreeAllocAny, WritesAny, [], [], [], []) }
| loop_annot_stack
    { $1 }
;

loop_effects:
| LOOP ASSIGNS full_assigns SEMICOLON { $3 }
;

loop_allocation:
| LOOP allocation SEMICOLON { $2 }
;

loop_invariant:
| LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred false $3 }
| CHECK_LOOP INVARIANT full_lexpr SEMICOLON { toplevel_pred true $3 }
;

loop_variant:
| LOOP VARIANT variant SEMICOLON { loc(),$3 }
;

/* Grammar Extensibility for plugins */
loop_grammar_extension:
| LOOP EXT_CODE_ANNOT grammar_extension SEMICOLON {
  let open Cil_types in
  let ext = $2 in
  try
    begin match Logic_env.extension_category ext with
      | Ext_code_annot (Ext_next_loop | Ext_next_both) ->
        let processed = Logic_env.preprocess_extension ext $3 in
        (ext, processed)
      | Ext_code_annot (Ext_here | Ext_next_stmt) ->
        raise
          (Not_well_formed
            (lexeme_loc 2, ext ^ " is not a loop annotation extension"))
      | _ -> raise Not_found
    end
  with Not_found ->
    Kernel.fatal ~source:(lexeme_start 2)
      "%s is not a code annotation extension. Parser got wrong lexeme." ext
}
;

loop_pragma:
| LOOP PRAGMA any_identifier full_ne_lexpr_list SEMICOLON
  { if $3 = "UNROLL_LOOP" || $3 = "UNROLL" then
      (if $3 <> "UNROLL" then
	 Format.eprintf "Warning: use of deprecated keyword '%s'.\nShould use 'UNROLL' instead.@." $3;
       Unroll_specs $4)
    else if $3 = "WIDEN_VARIABLES" then
      Widen_variables $4
    else if $3 = "WIDEN_HINTS" then
      Widen_hints $4
    else raise (Not_well_formed (loc(),"Unknown loop pragma")) }
;

/*** code annotations ***/

beg_pragma_or_code_annotation:
| IMPACT {}
| SLICE {}
| FOR {}
| ASSERT {}
| CHECK {}
| INVARIANT {}
| CHECK_INVARIANT {}
| EXT_CODE_ANNOT {}
;

pragma_or_code_annotation:
| slice_pragma     { APragma (Slice_pragma $1) }
| impact_pragma    { APragma (Impact_pragma $1) }
| code_annotation  { $1 []  }
;

code_annotation:
| ASSERT full_lexpr SEMICOLON
  { fun bhvs -> AAssert (bhvs,toplevel_pred false $2) }
| CHECK full_lexpr SEMICOLON
  { fun bhvs -> AAssert (bhvs,toplevel_pred true $2) }
| INVARIANT full_lexpr SEMICOLON
  { fun bhvs -> AInvariant (bhvs,false,toplevel_pred false $2) }
| CHECK_INVARIANT full_lexpr SEMICOLON
  { fun bhvs -> AInvariant (bhvs,false,toplevel_pred true $2) }
| EXT_CODE_ANNOT grammar_extension SEMICOLON
  { fun bhvs ->
    let open Cil_types in
    let ext = $1 in
    try
      begin match Logic_env.extension_category ext with
        | Ext_code_annot (Ext_here | Ext_next_stmt | Ext_next_both) ->
          let processed = Logic_env.preprocess_extension ext $2 in
          Logic_ptree.AExtended(bhvs,false,(ext,processed))
        | Ext_code_annot Ext_next_loop ->
          raise
            (Not_well_formed
               (lexeme_loc 1,
                 ext ^ " is not a loop annotation extension. It can't be used \
                         as plain code annotation extension"))
        | _ -> raise Not_found
      end
    with Not_found ->
      Kernel.fatal ~source:(lexeme_start 1)
        "%s is not a code annotation extension. Parser got wrong lexeme" ext
  }
;

slice_pragma:
| SLICE PRAGMA any_identifier full_lexpr SEMICOLON
    { if $3 = "expr" then SPexpr $4
      else raise (Not_well_formed (loc(), "Unknown slice pragma")) }
| SLICE PRAGMA any_identifier SEMICOLON
    { if $3 = "ctrl" then SPctrl
      else if $3 = "stmt" then SPstmt
      else raise (Not_well_formed (loc(), "Unknown slice pragma")) }
;

impact_pragma:
| IMPACT PRAGMA any_identifier full_lexpr SEMICOLON
    { if $3 = "expr" then IPexpr $4
      else raise (Not_well_formed (loc(), "Unknown impact pragma")) }
| IMPACT PRAGMA any_identifier SEMICOLON
    { if $3 = "stmt" then IPstmt
      else raise (Not_well_formed (loc(), "Unknown impact pragma")) }
;

/*** declarations and logical definitions ***/

decl_list:
| decl            { [loc_decl $1] }
| decl decl_list  { (loc_decl $1) :: $2 }

decl:
| GLOBAL INVARIANT any_identifier COLON full_lexpr SEMICOLON
    { LDinvariant ($3, $5) }
| VOLATILE full_ne_zones volatile_opt SEMICOLON { LDvolatile ($2, $3) }
| type_annot {LDtype_annot $1}
| model_annot {LDmodel_annot $1}
| logic_def  { $1 }
| EXT_GLOBAL grammar_extension SEMICOLON {
    let processed = Logic_env.preprocess_extension $1 $2 in
	  LDextended ($1, processed)
  }
| deprecated_logic_decl { $1 }
;

volatile_opt:
| /* empty */ { None, None }
| READS any_identifier volatile_opt
              { let read,write=$3 in
                  if read = None then
		    (Some $2),write
		  else
                    (Format.eprintf "Warning: read %s ignored@." $2; $3)
	      }
| WRITES any_identifier volatile_opt
              { let read,write=$3 in
                  if write = None then
		    read,(Some $2)
		  else
                    (Format.eprintf "Warning: write %s ignored@." $2; $3)
	      }
;

type_annot:
| TYPE INVARIANT any_identifier LPAR full_parameter RPAR EQUAL
    full_lexpr SEMICOLON
  { let typ,name = $5 in{ inv_name = $3; this_name = name; this_type = typ; inv = $8; } }
;

opt_semicolon:
| /* epsilon */ { }
| SEMICOLON { }

model_annot:
| MODEL type_spec LBRACE full_parameter opt_semicolon RBRACE SEMICOLON
  { let typ,name = $4 in
    { model_for_type = $2; model_name = name; model_type = typ; }
  }
;

poly_id_type:
| full_identifier
    { enter_type_variables_scope []; ($1,[]) }
| full_identifier LT ne_tvar_list GT
        { enter_type_variables_scope $3; ($1,$3) }
;

/* we need to recognize the typename as soon as it has been declared,
  so that it can be used in data constructors in the type definition itself
*/
poly_id_type_add_typename:
| poly_id_type { let (id,_) = $1 in Logic_env.add_typename id; $1 }
;

poly_id:
| poly_id_type { let (id,tvar) = $1 in (id,[],tvar) }
| full_identifier LBRACE ne_label_list RBRACE
      { enter_type_variables_scope []; ($1,$3,[]) }
| full_identifier LBRACE ne_label_list RBRACE LT ne_tvar_list GT
      { enter_type_variables_scope $6; $1,$3,$6 }
;

opt_parameters:
| /*epsilon*/ { [] }
| parameters { $1 }
;

parameters:
| LPAR full_parameters RPAR { $2 }
;

logic_def:
/* logic function definition */
| LOGIC full_logic_rt_type poly_id opt_parameters EQUAL full_lexpr SEMICOLON
    { let (id, labels, tvars) = $3 in
      exit_type_variables_scope ();
      LDlogic_def (id, labels, tvars, $2, $4, $6) }
/* predicate definition */
| PREDICATE poly_id opt_parameters EQUAL full_lexpr SEMICOLON
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      LDpredicate_def (id, labels, tvars, $3, $5) }
/* inductive predicate definition */
| INDUCTIVE poly_id parameters LBRACE indcases RBRACE
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      LDinductive_def(id, labels, tvars, $3, $5) }
| LEMMA poly_id COLON full_lexpr SEMICOLON
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      LDlemma (id, false, labels, tvars, toplevel_pred false $4) }
| CHECK_LEMMA poly_id COLON full_lexpr SEMICOLON
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      LDlemma (id, false, labels, tvars, toplevel_pred true $4) }
| AXIOMATIC any_identifier LBRACE logic_decls RBRACE
    { LDaxiomatic($2,$4) }
| TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
        { let (id,tvars) = $2 in
          exit_type_variables_scope ();
          LDtype(id,tvars,Some $4)
        }
;

deprecated_logic_decl:
/* OBSOLETE: logic function declaration */
| LOGIC full_logic_rt_type poly_id opt_parameters SEMICOLON
    { let (id, labels, tvars) = $3 in
      let source = fst (loc ()) in
      exit_type_variables_scope ();
      obsolete  "logic declaration" ~source ~now:"an axiomatic block";
      LDlogic_reads (id, labels, tvars, $2, $4, None) }
/* OBSOLETE: predicate declaration */
| PREDICATE poly_id opt_parameters SEMICOLON
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      let source = fst (loc ()) in
      obsolete "logic declaration" ~source ~now:"an axiomatic block";
      LDpredicate_reads (id, labels, tvars, $3, None) }
/* OBSOLETE: type declaration */
| TYPE poly_id_type SEMICOLON
    { let (id,tvars) = $2 in
      Logic_env.add_typename id;
      exit_type_variables_scope ();
      let source = fst (loc ()) in
      obsolete "logic type declaration" ~source ~now:"an axiomatic block";
      LDtype(id,tvars,None)
    }
/* OBSOLETE: axiom */
| AXIOM poly_id COLON full_lexpr SEMICOLON
    { let (id,_,_) = $2 in
      raise
	(Not_well_formed
	   (loc(),"Axiom " ^ id ^ " is declared outside of an axiomatic."))
    }
;


logic_decls:
| /* epsilon */
    { [] }
| logic_decl_loc logic_decls
    { $1::$2 }
;

logic_decl:
| logic_def  { $1 }
/* logic function declaration */
| LOGIC full_logic_rt_type poly_id opt_parameters reads_clause SEMICOLON
    { let (id, labels, tvars) = $3 in
      exit_type_variables_scope ();
      LDlogic_reads (id, labels, tvars, $2, $4, $5) }
/* predicate declaration */
| PREDICATE poly_id opt_parameters reads_clause SEMICOLON
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      LDpredicate_reads (id, labels, tvars, $3, $4) }
/* type declaration */
| TYPE poly_id_type SEMICOLON
    { let (id,tvars) = $2 in
      Logic_env.add_typename id;
      exit_type_variables_scope ();
      LDtype(id,tvars,None) }
/* axiom */
| AXIOM poly_id COLON full_lexpr SEMICOLON
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      LDlemma (id, true, labels, tvars, toplevel_pred false $4) }
;

logic_decl_loc:
| logic_decl { loc_decl $1 }
;


reads_clause:
| /* epsilon */ { None }
| READS full_zones { Some $2 }
;

typedef:
| ne_datacons_list { TDsum $1 }
| full_logic_type { TDsyn $1 }
;

datacons_list:
| /* epsilon */ { [] }
| PIPE datacons datacons_list { $2 :: $3 }
;

ne_datacons_list:
| datacons datacons_list { $1 :: $2 }
| PIPE datacons datacons_list { $2 :: $3 }
;

datacons:
| full_identifier { ($1,[]) }
| full_identifier LPAR ne_type_list RPAR { ($1,$3) }
;

ne_type_list:
| full_logic_type { [$1] }
| full_logic_type COMMA ne_type_list { $1::$3 }

indcases:
| /* epsilon */
    { [] }
| CASE poly_id COLON full_lexpr SEMICOLON indcases
    { let (id,labels,tvars) = $2 in
      exit_type_variables_scope ();
      (id,labels,tvars,$4)::$6 }
;


ne_tvar_list:
| full_identifier                    { [$1] }
| full_identifier COMMA ne_tvar_list { $1 :: $3 }
;

ne_label_list:
| label_name                     { [$1] }
| label_name COMMA ne_label_list { $1 :: $3 }
;

opt_label_1:
| opt_label_list { match $1 with
		     | [] -> None
		     | l::[] -> Some l
		     | _ -> raise (Not_well_formed (loc(),"Only one label is allowed")) }
;

opt_label_2:
| opt_label_list { match $1 with
		     | [] -> None
		     | l1::l2::[] -> Some (l1,l2)
		     | _::[] -> raise (Not_well_formed (loc(),"One label is missing"))
		     | _ -> raise (Not_well_formed (loc(),"Only two labels are allowed")) }
;

opt_label_list:
| /* epsilon */               { [] }
| LBRACE ne_label_list RBRACE { $2 }
;

/* names */
label_name:
| any_identifier { $1 }
;

behavior_name_list:
| /* epsilon */         { [] }
| ne_behavior_name_list { $1 }
;

ne_behavior_name_list:
| behavior_name                             { [$1] }
| behavior_name COMMA ne_behavior_name_list {$1 :: $3}
;

behavior_name:
| any_identifier { $1 }
;

any_identifier:
| identifier_or_typename { $1 }
| keyword { $1 }
;

any_identifier_non_logic:
| identifier_or_typename { $1 }
| non_logic_keyword { $1 }

identifier_or_typename: /* allowed as C field names */
| TYPENAME { $1 } /* followed by the same list than 'identifier' */
| IDENTIFIER { $1 }
/* token list used inside ascl clauses: */
| BEHAVIORS  { "behaviors" }
| LABEL      { "label" }
| READS      { "reads" }
| WRITES     { "writes" }
;

identifier: /* part included into 'identifier_or_typename', but duplicated to avoid parsing conflicts */
| IDENTIFIER { $1 }
/* token list used inside ascl clauses: */
| BEHAVIORS  { "behaviors" }
| LABEL      { "label" }
| READS      { "reads" }
| WRITES     { "writes" }
;

bounded_var:
| identifier { $1 }
| TYPENAME  /* Since TYPENAME cannot be accepted by lexpr rule */
    { raise
	(Not_well_formed(loc (),
			 "Type names are not allowed as binding variable"))
    }
;

c_keyword:
| CHAR     { "char" }
| BOOLEAN  { "boolean" }
| BOOL     { "_Bool" }
| CONST    { "const" }
| DOUBLE   { "double" }
| ENUM     { "enum" }
| ELSE     { "else" }
| FLOAT    { "float" }
| IF       { "if" }
| INT      { "int" }
| LONG     { "long" }
| SHORT    { "short" }
| SIGNED   { "signed" }
| SIZEOF   { "sizeof" }
| STATIC   { "static" }
| STRUCT   { "struct" }
| UNION    { "union" }
| UNSIGNED { "unsigned" }
| VOID     { "void" }
;

acsl_c_keyword:
| CASE     { "case" }
| FOR      { "for" }
| VOLATILE { "volatile" }
;

post_cond:
| ENSURES { (false,Normal), "ensures" }
| EXITS   { (false,Exits), "exits" }
| BREAKS  { (false,Breaks), "breaks" }
| CONTINUES { (false,Continues), "continues" }
| RETURNS { (false,Returns), "returns" }
| CHECK_ENSURES { (true,Normal), "check ensures" }
| CHECK_EXITS   { (true,Exits), "check exits" }
| CHECK_BREAKS  { (true,Breaks), "check breaks" }
| CHECK_CONTINUES { (true,Continues), "check continues" }
| CHECK_RETURNS { (true,Returns), "check returns" }
;

is_acsl_spec:
| post_cond  { snd $1 }
| EXT_CONTRACT   { $1 }
| ASSIGNS    { "assigns" }
| ALLOCATES  { "allocates" }
| FREES      { "frees" }
| BEHAVIOR   { "behavior" }
| REQUIRES   { "requires" }
| CHECK_REQUIRES { "check requires" }
| TERMINATES { "terminates" }
| COMPLETE   { "complete" }
| DECREASES  { "decreases" }
| DISJOINT   { "disjoint" }
;

is_acsl_decl_or_code_annot:
| EXT_CODE_ANNOT { $1 }
| EXT_GLOBAL     { $1 }
| ASSUMES   { "assumes" }
| ASSERT    { "assert" }
| CHECK     { "check" }
| GLOBAL    { "global" }
| IMPACT    { "impact" }
| INDUCTIVE { "inductive" }
| INVARIANT { "invariant" }
| LEMMA     { "lemma" }
| LOOP      { "loop" }
| PRAGMA    { "pragma" }
| PREDICATE { "predicate" }
| SLICE     { "slice" }
| TYPE      { "type" }
| MODEL     { "model" }
| AXIOM     { "axiom" }
| VARIANT   { "variant" }
| AXIOMATIC { "axiomatic" }
;

is_acsl_other:
| INTEGER  { "integer" (* token that cannot be used in C fields *) }
| REAL     { "real" (* token that cannot be used in C fields *) }
;

is_ext_spec:
| CONTRACT { "contract" }
| FUNCTION { "function" }
| MODULE   { "module" }
| INCLUDE  { "include" }
| EXT_AT   { "at" }
| EXT_LET  { "let" }
;

keyword:
| LOGIC   { "logic" }
| non_logic_keyword { $1 }
;

non_logic_keyword:
| c_keyword      { $1 }
| acsl_c_keyword { $1 }
| is_ext_spec    { $1 }
| is_acsl_spec   { $1 }
| is_acsl_decl_or_code_annot { $1 }
| is_acsl_other  { $1 }
| CUSTOM { "custom" (* token that cannot be used in C fields *) }
;

bs_keyword:
| ALLOCABLE { () }
| ALLOCATION { () }
| AUTOMATIC { () }
| AT { () }
| BASE_ADDR { () }
| BLOCK_LENGTH { () }
| DYNAMIC { () }
| EMPTY { () }
| FALSE { () }
| FORALL { () }
| FREEABLE { () }
| FRESH { () }
| FROM { () }
| INTER { () }
| LAMBDA { () }
| LET { () }
| NOTHING { () }
| NULL { () }
| OLD { () }
| OFFSET { () }
| REGISTER { () }
| RESULT { () }
| SEPARATED { () }
| TRUE { () }
| BSTYPE { () }
| TYPEOF { () }
| BSUNION { () }
| UNALLOCATED { () }
| OBJECT_POINTER { () }
| VALID { () }
| VALID_INDEX { () }
| VALID_RANGE { () }
| VALID_READ { () }
| VALID_FUNCTION { () }
| INITIALIZED { () }
| DANGLING { () }
| WITH { () }
;

wildcard:
| any_identifier { () }
| bs_keyword { () }
| AMP { () }
| AND { () }
| ARROW { () }
| BIFF { () }
| BIMPLIES { () }
| COLON { () }
| COLON2 { () }
| COLONCOLON { () }
| COMMA { () }
| CONSTANT { () }
| CONSTANT10 { () }
| DOLLAR { () }
| DOT { () }
| DOTDOT { () }
| DOTDOTDOT { () }
| EQ { () }
| EQUAL { () }
| EXISTS { () }
| GE { () }
| GHOST { () }
| GT { () }
| GTGT { () }
| HAT { () }