logic_parser.mly

/**************************************************************************/
/*                                                                        */
/*  This file is part of Frama-C.                                         */
/*                                                                        */
/*  Copyright (C) 2007-2025                                               */
/*    CEA   (Commissariat à l'énergie atomique et aux énergies            */
/*           alternatives)                                                */
/*    INRIA (Institut National de Recherche en Informatique et en         */
/*           Automatique)                                                 */
/*                                                                        */
/*  you can redistribute it and/or modify it under the terms of the GNU   */
/*  Lesser General Public License as published by the Free Software       */
/*  Foundation, version 2.1.                                              */
/*                                                                        */
/*  It is distributed in the hope that it will be useful,                 */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
/*  GNU Lesser General Public License for more details.                   */
/*                                                                        */
/*  See the GNU Lesser General Public License version 2.1                 */
/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
/*                                                                        */
/**************************************************************************/

/* Grammar for C annotations */

%{

  open Cil_types
  open Logic_ptree
  open Logic_utils

  let loc (start_pos, end_pos) =
    Cil_datatype.Location.of_lexing_loc
      (start_pos, end_pos)

  let pos pos =
    Cil_datatype.Position.of_lexing_pos pos

  let loc_info lexpr_loc x = { lexpr_node = x; lexpr_loc }
  let loc_start x = fst x.lexpr_loc
  let loc_end x = snd x.lexpr_loc

  let info start_end x = loc_info (loc start_end) x

  (* Normalize p1 && (p2 && p3) into (p1 && p2) && p3 *)
  let rec pland p1 p2 =
    match p2.lexpr_node with
      | PLand (p3,p4) ->
        let loc = (loc_start p1, loc_end p3) in
        PLand(loc_info loc (pland p1 p3),p4)
      | _ -> PLand(p1,p2)

  let rec plor p1 p2 =
    match p2.lexpr_node with
      | PLor(p3,p4) ->
        let loc = (loc_start p1, loc_end p3) in
        PLor(loc_info loc (plor p1 p3),p4)
      | _ -> PLor(p1,p2)

  let clause_order start_end name1 name2 =
    raise
      (Not_well_formed
         (loc start_end,
          "wrong order of clause in contract: "
          ^ name1 ^ " after " ^ name2 ^ "."))

  let missing start_end token next_token =
    raise
      (Not_well_formed
         (loc start_end,
          Format.asprintf "expecting '%s' before %s" token next_token))

  type sense_of_relation = Unknown | Disequal | Less | Greater

  let check_empty (loc,msg) l =
    match l with
        [] -> ()
      | _ -> raise (Not_well_formed (loc,msg))

  let relation_sense rel sense =
    match rel, sense with
      | Eq, (Unknown|Greater|Less) -> sense, true
      | Neq, Unknown -> Disequal, false (* No chain of disequality for now*)
      | (Gt|Ge), (Unknown|Greater) -> Greater, true
      | (Lt|Le), (Unknown|Less) -> Less, true
      | _ -> sense, false

  let module_types : string list ref Stack.t = Stack.create ()

  let push_typename t =
    Logic_env.add_typename t ;
    try
      let r = Stack.top module_types in r := t :: !r
    with Stack.Empty -> ()

  let push_module_types () =
    Stack.push (ref []) module_types

  let pop_module_types () =
    let r = Stack.pop module_types in
    List.iter Logic_env.remove_typename !r

  let type_variables_stack = Stack.create ()

  let enter_type_variables_scope l =
    List.iter Logic_env.add_typename l;
    Stack.push l type_variables_stack

  let exit_type_variables_scope () =
    let l = Stack.pop type_variables_stack in
    List.iter Logic_env.remove_typename l

  let loc_decl start_end d = { decl_node = d; decl_loc = loc start_end }

  let loc_ext start_end d = { extended_node = d; extended_loc = loc start_end }

  let filter_from l = function
    | FromAny ->
      l, FromAny
    | From ds ->
      let f ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in
      l, From(List.(rev (fold_left f [] ds)))

  let concat_froms cura newa =
    let compare_pair (curb,_) (newb,_) = is_same_lexpr curb newb in
    (* NB: the following has an horrible complexity, but the order of
       clauses in the input is preserved. *)
    let concat_one acc (newloc, newf)  =
      let (newloc, newf) as p = filter_from newloc newf in
      try
        let (curloc,curf) = List.find (compare_pair p) acc
        in
        match (curf, newf) with
          | _,FromAny ->
            (* the new fundeps does not give more information than the one
               which is already present. Just ignore it.
             *)
           acc
          | FromAny, _ ->
              (* the new fundeps is strictly more precise than the old one.
                 We replace the old dependency by the new one, but keep
                 the location at its old place in the list. This ensures
                 that we get the exact same clause if we try to
                 link the original contract with its pretty-printed version. *)
              Extlib.replace compare_pair p acc
          | From curl, From newl ->
            let incl l lin =
              List.(for_all (fun e -> exists (is_same_lexpr e) lin) l)
            in
            let drop d k =
              Kernel.warning ~current:false ~wkey:Kernel.wkey_multi_from
                "Drop '%a' \\from at %a for more precise one at %a"
                Logic_print.print_lexpr curloc
                Cil_datatype.Location.pretty d.lexpr_loc
                Cil_datatype.Location.pretty k.lexpr_loc
            in
            if incl curl newl then begin
              if not (incl newl curl) then drop newloc curloc;
              acc
            end
            else if incl newl curl then begin
              drop curloc newloc;
              Extlib.replace compare_pair p acc
            end
            else acc @ [p]
      with Not_found -> acc @ [p]
    in List.fold_left concat_one cura newa

  let concat_allocation fa1 fa2 =
    match fa1,fa2 with
      | FreeAllocAny,_ -> fa2
      | _,FreeAllocAny -> fa1
      | FreeAlloc(f1,a1),FreeAlloc(f2,a2) -> FreeAlloc(f2@f1,a2@a1)

  (* a1 represents the assigns _after_ the current clause a2. *)
  let concat_assigns start_pos a1 a2 =
    match a1,a2 with
        WritesAny,a -> Writes (concat_froms [] a)
      | Writes [], [] -> a1
      | Writes [], _  | Writes _, [] ->
        raise (
          Not_well_formed (loc start_pos,"Mixing \\nothing and a real location"))
      | Writes a1, a2 -> Writes (concat_froms (concat_froms [] a2) a1)

  let concat_loop_assigns_allocation start_pos annots bhvs2 a2 fa2=
    (* NB: this is supposed to merge assigns related to named behaviors, in
       case of annotation like
       for a,b: assigns x,y;
       for b,c: assigns z,t;
       DO NOT CALL this function for loop assigns not attached to specific
       behaviors.
     *)
    assert (bhvs2 <> []);
    if fa2 == FreeAllocAny && a2 == WritesAny
    then annots
    else
    let split l1 l2 =
      let treat_one (only1,both,only2) x =
        if List.mem x l1 then
          (List.filter (fun y -> x <> y) only1,x::both,only2)
        else (only1,both,x::only2)
      in List.fold_left treat_one (l1,[],[]) l2
    in
    let treat_one ca (bhvs2,acc) =
      match ca,a2,fa2 with
          (AAssigns(bhvs1,a1)),(Writes a2),_ ->
            let (only1,both,only2) = split bhvs1 bhvs2 in
            (match both with
              | [] -> bhvs2, ca::acc
              | _ ->
                let common_annot = AAssigns(both,concat_assigns start_pos a1 a2) in
                let annots =
                  match only1 with
                    | [] -> common_annot :: acc
                    | _ -> AAssigns(only1,a1) :: common_annot :: acc
                in only2,annots)
        | (AAllocation(bhvs1,fa1)),_,(FreeAlloc _) ->
           let (only1,both,only2) = split bhvs1 bhvs2 in
            (match both with
              | [] -> bhvs2, ca::acc
              | _ ->
                let common_annot =
                  AAllocation(both,concat_allocation fa1 fa2)
                in
                let annots =
                  match only1 with
                    | [] -> common_annot :: acc
                    | _ -> AAllocation(only1,fa1) :: common_annot :: acc
                in only2,annots)
         | _,_,_ -> bhvs2,ca::acc
    in
    let (bhvs2, annots) = List.fold_right treat_one annots (bhvs2,[]) in
    match bhvs2 with
      | [] -> annots (* Already considered all cases. *)
      | _ ->
	  let annots = if a2 <> WritesAny
	    then AAssigns (bhvs2,a2) :: annots
            else annots
	  in
	  if fa2 <> FreeAllocAny
	    then AAllocation (bhvs2,fa2) :: annots
            else annots

  let obsolete name ~source ~now =
    Kernel.warning ~source
      "parsing obsolete ACSL construct '%s'. '%s' should be used instead."
      name now

  let escape =
    let regex1 = Str.regexp "\\(\\(\\\\\\\\\\)*[^\\]\\)\\(['\"]\\)" in
    let regex2 = Str.regexp "\\(\\\\\\\\\\)*\\\\$" in
    fun str ->
      let str = Str.global_replace regex1 "\\1\\\\3" str in
      Str.global_replace regex2 "\\1\\\\" str

  let cv_const = ("const", [])
  let cv_volatile = ("volatile", [])
  let cv_ghost = ("ghost", [])

  let toplevel_pred tp_kind tp_statement = { tp_kind; tp_statement }

  let extension ext_name ext_plugin ext_content =
    {ext_name; ext_plugin; ext_content}

  let global_extension gext_name gext_plugin gext_kind gext_content =
    Ext_extension {gext_name; gext_plugin; gext_kind; gext_content}

  let import loader module_name module_alias =
    let import_loader =
      match loader with
      | None -> None
      | Some (loader_name, loader_plugin) ->
          Some {loader_name;loader_plugin}
    in
    LDimport { import_loader; module_name; module_alias}


%}

/*****************************************************************************/
/* IMPORTANT NOTE: When you add a new token, be sure that it will be         */
/* recognized by the any: rule at the end of this file.                      */
/* Otherwise, the token will not be usable inside a contract.                */
/*****************************************************************************/

%token EXT_SPEC_MODULE EXT_SPEC_FUNCTION EXT_SPEC_CONTRACT EXT_SPEC_INCLUDE
%token EXT_SPEC_AT EXT_SPEC_LET
%token <string> LONGIDENT IDENTIFIER TYPENAME IDENTIFIER_EXT IDENTIFIER_LOADER
%token <bool*string> STRING_LITERAL
%token <string> INT_CONSTANT
%token <string> FLOAT_CONSTANT
%token <string> STRING_CONSTANT
%token <string> WSTRING_CONSTANT
%token LPAR RPAR IF ELSE COLON COLON2 COLONCOLON DOT DOTDOT DOTDOTDOT
%token INT INTEGER REAL BOOLEAN BOOL FLOAT LT GT LE GE EQ NE COMMA ARROW EQUAL
%token FORALL EXISTS IFF IMPLIES AND OR NOT SEPARATED
%token TRUE FALSE OLD AS AT RESULT
%token BLOCK_LENGTH BASE_ADDR OFFSET VALID VALID_READ VALID_INDEX VALID_RANGE
%token OBJECT_POINTER VALID_FUNCTION
%token ALLOCATION STATIC REGISTER AUTOMATIC DYNAMIC UNALLOCATED
%token ALLOCABLE FREEABLE FRESH
%token DOLLAR QUESTION MINUS PLUS STAR AMP SLASH PERCENT LSQUARE RSQUARE EOF
%token GLOBAL INVARIANT VARIANT DECREASES FOR LABEL ASSERT CHECK ADMIT SEMICOLON NULL EMPTY
%token REQUIRES ENSURES ALLOCATES FREES ASSIGNS LOOP NOTHING FROM
%token CHECK_REQUIRES CHECK_LOOP CHECK_INVARIANT CHECK_LEMMA
%token CHECK_ENSURES CHECK_EXITS CHECK_CONTINUES CHECK_BREAKS CHECK_RETURNS
%token ADMIT_REQUIRES ADMIT_LOOP ADMIT_INVARIANT ADMIT_LEMMA
%token ADMIT_ENSURES ADMIT_EXITS ADMIT_CONTINUES ADMIT_BREAKS ADMIT_RETURNS
%token <string * string> EXT_CODE_ANNOT EXT_GLOBAL EXT_GLOBAL_BLOCK EXT_CONTRACT EXT_LOADER EXT_LOADER_PLUGIN
%token EXITS BREAKS CONTINUES RETURNS
%token VOLATILE READS WRITES
%token LOGIC PREDICATE INDUCTIVE AXIOM LEMMA LBRACE RBRACE
%token AXIOMATIC MODULE IMPORT
%token MODEL CASE
%token VOID CHAR SIGNED UNSIGNED SHORT LONG DOUBLE STRUCT ENUM UNION
%token BSUNION INTER
%token TYPE BEHAVIOR BEHAVIORS ASSUMES COMPLETE DISJOINT
%token TERMINATES
%token BIFF BIMPLIES STARHAT HAT HATHAT PIPE TILDE GTGT LTLT
%token SIZEOF LAMBDA LET
%token TYPEOF BSTYPE
%token WITH CONST GHOST
%token INITIALIZED DANGLING
%token LSQUAREPIPE RSQUAREPIPE
%token IN
%token PI

%right prec_named
%nonassoc prec_forall prec_exists prec_lambda LET
%right QUESTION prec_question
%left IFF
%right IMPLIES
%left OR
%left HATHAT
%left AND
%left BIFF
%right BIMPLIES
%left PIPE
%left HAT
%left STARHAT
%left AMP
%nonassoc IN
%left LTLT GTGT
%left PLUS MINUS
%left STAR SLASH PERCENT
%right prec_cast TILDE NOT prec_unary_op
%left DOT ARROW LSQUARE

%type <Logic_ptree.lexpr> lexpr_eof
%start lexpr_eof

%type <Logic_ptree.annot> annot
%start annot

%type <Logic_ptree.spec> spec
%start spec

%type <Logic_ptree.ext_spec> ext_spec
%start ext_spec

%%

/*** predicates and terms ***/

lexpr_list:
| /* epsilon */ { [] }
| ne_lexpr_list  { $1 }
;

ne_lexpr_list:
| lexpr                    { [$1] }
| lexpr COMMA ne_lexpr_list { $1 :: $3 }
;

lexpr_eof:
| lexpr EOF { $1 }
;

lexpr_option:
| /* epsilon */ { None }
| lexpr         { Some $1 }
;

lexpr:
  /* predicates */
| lexpr IMPLIES lexpr { info $sloc (PLimplies ($1, $3)) }
| lexpr IFF lexpr { info $sloc (PLiff ($1, $3)) }
| lexpr OR lexpr     { info $sloc (plor $1 $3) }
| lexpr AND lexpr    { info $sloc (pland $1 $3) }
| lexpr HATHAT lexpr    { info $sloc (PLxor ($1, $3)) }
/* terms */
| lexpr AMP lexpr { info $sloc (PLbinop ($1, Bbw_and, $3)) }
| lexpr PIPE lexpr { info $sloc (PLbinop ($1, Bbw_or, $3)) }
| lexpr HAT lexpr { info $sloc (PLbinop ($1, Bbw_xor, $3)) }
| lexpr BIMPLIES lexpr { info $sloc (PLbinop (info $sloc (PLunop (Ubw_not, $1)), Bbw_or, $3)) }
| lexpr BIFF lexpr { info $sloc (PLbinop (info $sloc (PLunop (Ubw_not, $1)), Bbw_xor, $3)) }
| lexpr IN lexpr { info $sloc (PLapp ("\\subset", [], [info $sloc (PLset [$1]);$3])) }
| lexpr QUESTION lexpr COLON2 lexpr %prec prec_question
    { info $sloc (PLif ($1, $3, $5)) }
/* both terms and predicates */
| any_identifier COLON lexpr %prec prec_named { info $sloc (PLnamed ($1, $3)) }
| string COLON lexpr %prec prec_named
      { let (iswide,str) = $1 in
        if iswide then begin
           let l = loc $sloc in
           raise (Not_well_formed(l, "Wide strings are not allowed as labels."))
         end;
        let str = escape str in
         info $sloc (PLnamed (str, $3))
       }
| lexpr_rel { $1 }
;

lexpr_rel:
| lexpr_end_rel  { $1 }
| lexpr_inner rel_list
      { let rel, rhs, _, oth_rel = $2 in
        let loc = loc_start $1, loc_end rhs in
        let relation = loc_info loc (PLrel($1,rel,rhs)) in
        match oth_rel with
            None -> relation
          | Some oth_relation -> info $sloc (pland relation oth_relation)
      }
;

lexpr_binder:
| LET bounded_var EQUAL lexpr SEMICOLON lexpr %prec LET
      { info $sloc (PLlet($2,$4,$6))}
| FORALL binders SEMICOLON lexpr  %prec prec_forall
      { info $sloc (PLforall ($2, $4)) }
| EXISTS binders SEMICOLON lexpr  %prec prec_exists
      { info $sloc (PLexists ($2, $4)) }
| LAMBDA binders SEMICOLON lexpr  %prec prec_lambda
      { info $sloc (PLlambda ($2,$4)) }
;

lexpr_end_rel:
  lexpr_inner  { $1 }
| lexpr_binder { $1 }
| NOT lexpr_binder { info $sloc (PLnot $2) }
;

rel_list:
| relation lexpr_end_rel
  { $1, $2, fst(relation_sense $1 Unknown), None }
| relation lexpr_inner rel_list
  {
    let next_rel, rhs, sense, oth_rel = $3 in
    let (sense, correct) = relation_sense $1 sense
    in
    if correct then
      let loc = loc_start $2, loc_end rhs in
      let my_rel = loc_info loc (PLrel($2,next_rel,rhs)) in
      let oth_rel = match oth_rel with
          None -> my_rel
        | Some rel ->
	    let loc = loc_start $2, loc_end rel in
	    loc_info loc (pland my_rel rel)
      in
      $1,$2,sense,Some oth_rel
    else begin
      let loc = loc $sloc in
      raise (Not_well_formed(loc,"Inconsistent relation chain."));
    end
  }
;

relation:
| LT    { Lt }
| GT    { Gt }
| LE    { Le }
| GE    { Ge }
| EQ    { Eq }
| NE    { Neq }
    /* C. Marche: added to produce better error messages */
| EQUAL {
      let l = loc $sloc in
      raise
        (Not_well_formed(l,
                         "Assignment operators not allowed in annotations."))
    }
;

lexpr_inner:
| string {
      let (is_wide,content) = $1 in
      let cst = if is_wide then
        WStringConstant content
      else
        StringConstant content
      in
      info $sloc (PLconstant cst)
    }
| NOT lexpr_inner { info $sloc (PLnot $2) }
| TRUE { info $sloc PLtrue }
| FALSE { info $sloc PLfalse }
| OBJECT_POINTER opt_label_1 LPAR lexpr RPAR { info $sloc (PLobject_pointer ($2,$4)) }
| VALID opt_label_1 LPAR lexpr RPAR { info $sloc (PLvalid ($2,$4)) }
| VALID_READ opt_label_1 LPAR lexpr RPAR { info $sloc (PLvalid_read ($2,$4)) }
| VALID_FUNCTION LPAR lexpr RPAR { info $sloc (PLvalid_function $3) }
| VALID_INDEX opt_label_1 LPAR lexpr COMMA lexpr RPAR {
  let source = pos $symbolstartpos in
  obsolete ~source "\\valid_index(addr,idx)" ~now:"\\valid(addr+idx)";
  info $sloc (PLvalid ($2,info $sloc (PLbinop ($4, Badd, $6)))) }
| VALID_RANGE opt_label_1 LPAR lexpr COMMA lexpr COMMA lexpr RPAR {
  let source = pos $symbolstartpos in
  obsolete "\\valid_range(addr,min,max)"
    ~source ~now:"\\valid(addr+(min..max))";
  info $sloc (PLvalid
          ($2,info $sloc (PLbinop ($4, Badd, (info $sloc (PLrange((Some $6),Some $8)))))))
}
| INITIALIZED opt_label_1 LPAR lexpr RPAR { info $sloc (PLinitialized ($2,$4)) }
| DANGLING opt_label_1 LPAR lexpr RPAR { info $sloc (PLdangling ($2,$4)) }
| FRESH opt_label_2 LPAR lexpr COMMA lexpr RPAR { info $sloc (PLfresh ($2,$4, $6)) }
| BASE_ADDR opt_label_1 LPAR lexpr RPAR { info $sloc (PLbase_addr ($2,$4)) }
| BLOCK_LENGTH opt_label_1 LPAR lexpr RPAR { info $sloc (PLblock_length ($2,$4)) }
| OFFSET opt_label_1 LPAR lexpr RPAR { info $sloc (PLoffset ($2,$4)) }
| ALLOCABLE opt_label_1 LPAR lexpr RPAR { info $sloc (PLallocable ($2,$4)) }
| FREEABLE opt_label_1 LPAR lexpr RPAR { info $sloc (PLfreeable ($2,$4)) }
| ALLOCATION opt_label_1 LPAR lexpr RPAR
  { let source = pos $symbolstartpos in
    Kernel.not_yet_implemented ~source "\\allocation" }
| AUTOMATIC {
  let source = pos $symbolstartpos in
  Kernel.not_yet_implemented ~source "\\automatic" }
| DYNAMIC {
  let source = pos $symbolstartpos in
  Kernel.not_yet_implemented ~source "\\dynamic" }
| REGISTER {
  let source = pos $symbolstartpos in
  Kernel.not_yet_implemented ~source "\\register" }
| STATIC {
  let source = pos $symbolstartpos in
  Kernel.not_yet_implemented ~source "\\static" }
| UNALLOCATED {
  let source = pos $symbolstartpos in
  Kernel.not_yet_implemented ~source "\\unallocated" }
| NULL { info $sloc PLnull }
| constant { info $sloc (PLconstant $1) }
| lexpr_inner PLUS lexpr_inner { info $sloc (PLbinop ($1, Badd, $3)) }
| lexpr_inner MINUS lexpr_inner { info $sloc (PLbinop ($1, Bsub, $3)) }
| lexpr_inner STAR lexpr_inner { info $sloc (PLbinop ($1, Bmul, $3)) }
| lexpr_inner SLASH lexpr_inner { info $sloc (PLbinop ($1, Bdiv, $3)) }
| lexpr_inner PERCENT lexpr_inner { info $sloc (PLbinop ($1, Bmod, $3)) }
| lexpr_inner STARHAT lexpr_inner  { info $sloc (PLrepeat ($1, $3)) }
| lexpr_inner ARROW identifier_or_typename_full { info $sloc (PLarrow ($1, $3)) }
| lexpr_inner DOT identifier_or_typename_full { info $sloc (PLdot ($1, $3)) }
| lexpr_inner LSQUARE range RSQUARE { info $sloc (PLarrget ($1, $3)) }
| lexpr_inner LSQUARE lexpr RSQUARE { info $sloc (PLarrget ($1, $3)) }
| LSQUAREPIPE lexpr_list RSQUAREPIPE { info $sloc (PLlist $2) }
| MINUS lexpr_inner %prec prec_unary_op { info $sloc (PLunop (Uminus, $2)) }
| PLUS  lexpr_inner %prec prec_unary_op { $2 }
| TILDE lexpr_inner { info $sloc (PLunop (Ubw_not, $2)) }
| STAR  lexpr_inner %prec prec_unary_op { info $sloc (PLunop (Ustar, $2)) }
| AMP   lexpr_inner %prec prec_unary_op { info $sloc (PLunop (Uamp, $2)) }
| SIZEOF LPAR lexpr RPAR { info $sloc (PLsizeofE $3) }
| SIZEOF LPAR cast_logic_type RPAR { info $sloc (PLsizeof $3) }
| OLD LPAR lexpr RPAR { info $sloc (PLold $3) }
| AT LPAR lexpr COMMA label_name RPAR { info $sloc (PLat ($3, $5)) }
| RESULT { info $sloc PLresult }
| SEPARATED LPAR ne_lexpr_list RPAR
      { info $sloc (PLseparated $3) }
| symbol_identifier LPAR ne_lexpr_list RPAR
      { info $sloc (PLapp ($1, [], $3)) }
| symbol_identifier LBRACE ne_label_args RBRACE LPAR ne_lexpr_list RPAR
      { info $sloc (PLapp ($1, $3, $6)) }
| symbol_identifier LBRACE ne_label_args RBRACE
      { info $sloc (PLapp ($1, $3, [])) }
| symbol_identifier  { info $sloc (PLvar $1) }
| PI  { info $sloc (PLvar "\\pi") }
| lexpr_inner GTGT lexpr_inner { info $sloc (PLbinop ($1, Brshift, $3))}
| lexpr_inner LTLT lexpr_inner { info $sloc (PLbinop ($1, Blshift, $3))}
| LPAR lexpr RPAR { info $sloc $2.lexpr_node }
| LPAR range RPAR { info $sloc $2.lexpr_node }
| LPAR cast_logic_type RPAR lexpr_inner %prec prec_cast
      { info $sloc (PLcast ($2, $4)) }
| TYPEOF LPAR lexpr RPAR { info $sloc (PLtypeof $3) }
| BSTYPE LPAR type_spec(typename) RPAR { info $sloc (PLtype $3) }
| BSTYPE LPAR type_spec(typename) stars RPAR { info $sloc (PLtype ($4 $3)) }
    /* tsets */
| EMPTY { info $sloc PLempty }
| BSUNION LPAR lexpr_list RPAR { info $sloc (PLunion $3) }
| INTER LPAR lexpr_list RPAR { info $sloc (PLinter $3) }
| LBRACE RBRACE
      { info $sloc (PLset []) }
/* because LONGIDENT can be both a type name or a plain identifier,
   we can't have a full lexpr here, as there would be an ambiguity
   in { x | a::b * ...: should a::b be considered as a type (hence
   we are parsing a comprehension with a binder), or an identifier
   (hence, we are still parsing an lexpr).
*/
| LBRACE lexpr_inner RBRACE
      { info $sloc (PLset [$2]) }
| LBRACE lexpr_inner COMMA lexpr_list RBRACE
      { info $sloc (PLset ($2 :: $4)) }
| LBRACE lexpr_inner PIPE binders RBRACE
      { info $sloc (PLcomprehension ($2,$4,None)) }
| LBRACE lexpr_inner PIPE binders SEMICOLON lexpr RBRACE
      { info $sloc (PLcomprehension ($2,$4,Some $6)) }
    /* Aggregated object initialization */
| LBRACE field_init RBRACE
      { info $sloc (PLinitField($2)) }
| LBRACE array_init RBRACE
      { info $sloc (PLinitIndex($2)) }
| LBRACE lexpr_inner WITH update RBRACE
      { List.fold_left
	  (fun a (path,upd_val) -> info $sloc (PLupdate(a,path,upd_val))) $2 $4 }
/*
| LET bounded_var EQUAL lexpr SEMICOLON lexpr %prec LET { info $sloc (PLlet($2,$4,$6))}*/
;

ne_label_args:
| identifier_or_typename_full { [ $1 ] }
| identifier_or_typename_full COMMA ne_label_args { $1 :: $3 }

string:
| STRING_LITERAL { $1 }
| string STRING_LITERAL {
      let (is_wide,prefix) = $1 in
      let (is_wide2,suffix) = $2 in
      (is_wide || is_wide2, prefix ^ suffix)
    }
;

range:
| lexpr_option DOTDOT lexpr_option { info $sloc (PLrange($1,$3)) }
;

/*** Aggregated object initialization ***/

field_path_elt:
| DOT identifier_or_typename_full { $2 }
;
field_init_elt:
| field_path_elt EQUAL lexpr { ($1, $3) }
;

field_init:
| field_init_elt                  { [$1] }
| field_init_elt COMMA field_init { $1::$3 }
;

array_path_elt:
| LSQUARE lexpr RSQUARE      { $2 }
| LSQUARE range RSQUARE      { $2 }
;

array_init_elt:
| array_path_elt EQUAL lexpr { ($1, $3) }


array_init:
| array_init_elt                  { [$1] }
| array_init_elt COMMA array_init { $1::$3 }
;

/*** Functional update ***/
update:
| update_elt                  { [$1] }
| update_elt COMMA update { $1::$3 }
;

update_elt:
| path EQUAL lexpr                { $1, PLupdateTerm $3 }
| path EQUAL LBRACE WITH update RBRACE { $1, PLupdateCont $5 }
;

path:
| path_elt      { [$1] }
| path_elt path { $1::$2 }
;

path_elt:
| field_path_elt { PLpathField $1 }
| array_path_elt { PLpathIndex $1 }
;

/*** binders ***/

binders:
| binders_reentrance { let (_lt, vars) = $1 in vars }
;

binders_reentrance:
| decl_spec { let (lt, var) = $1 in (lt, [var]) }
| binders_reentrance COMMA decl_spec
    { let _, vars = $1 in
      let (lt, var) = $3 in
        (lt, vars @ [ var ])
    }
| binders_reentrance COMMA var_spec
    { let last_type_spec, vars = $1 in
        (last_type_spec, vars @ [ let (modif, name) = $3 in (modif last_type_spec, name)])
    }
;

decl_spec:
| type_spec(typesymbol) var_spec { ($1, let (modif, name) = $2 in (modif $1, name))  }
;

var_spec:
|       var_spec_bis { let (outer, inner,name) = $1 in
                       ((fun x -> outer (inner x)), name)}
| stars var_spec_bis
  { let (outer, inner, name) = $2 in
      ((fun x -> outer (inner ($1 x))), name) }
;

constant:
| INT_CONSTANT   { IntConstant $1 }
| FLOAT_CONSTANT { FloatConstant $1 }
| STRING_CONSTANT { StringConstant $1 }
| WSTRING_CONSTANT { WStringConstant $1 }
;

array_size:
| INT_CONSTANT { ASinteger $1 }
| full_identifier { ASidentifier $1 }
| /* empty */ { ASnone }
;

var_spec_bis:
| full_identifier     { ((fun x -> x),(fun x -> x), $1) }
| var_spec_bis LSQUARE array_size RSQUARE
      { let (outer, inner, name) = $1 in
          (outer, (fun x -> inner (LTarray (x,$3))), name)
      }
| LPAR var_spec RPAR { let (modif, name) = $2 in (modif, (fun x -> x), name) }
| var_spec_bis LPAR abs_param_type_list RPAR
      { let (outer, inner,name) = $1 in
        let params = $3 in
        (outer, (fun x -> inner (LTarrow (params,x))), name)
      }
;

abs_param_type_list:
| /* empty */    { [ ] }
| abs_param_list { $1 }
| abs_param_list COMMA DOTDOTDOT {
  let source = pos $symbolstartpos in
  Kernel.not_yet_implemented ~source "variadic C function types"
  }
;

abs_param_list:
| abs_param { [ $1 ] }
| abs_param_list COMMA abs_param { $1 @ [ $3 ] }
;

/* TODO: abs_param should be less restrictive than parameter
since its name can be omitted
*/
abs_param:
| logic_type { $1 }
;

ne_parameters:
| parameter { [$1] }
| parameter COMMA ne_parameters { $1 :: $3 }
;

parameter:
| type_spec(identifier_or_typename) var_spec
  { let (modif, name) = $2 in (modif $1, name)}
;


/*** type expressions ***/

logic_type_gen(tname):
| type_spec(tname) abs_spec_option { $2 $1 }
;

typename:
| name = TYPENAME { name }
;

typesymbol:
| name = TYPENAME { name }
| name = LONGIDENT { name }
/* TODO treat the case of an ACSL keyword that is also a typedef */
;

logic_type: logic_type_gen(typesymbol) { $1 }

cv:
  CONST { cv_const }
| VOLATILE { cv_volatile }
| GHOST { cv_ghost }
;

type_spec_cv:
     type_spec(TYPENAME) cv_after { $2 $1 }
|    cv type_spec_cv { LTattribute ($2, $1) }

cv_after:
  /* empty */ { fun t -> t }
| cv cv_after { fun t -> $2 (LTattribute (t,$1)) }

cast_logic_type:
 | type_spec_cv abs_spec_cv_option { $2 $1 }
;

logic_rt_type:
| logic_type_gen(identifier_or_typename) { $1 }
;

abs_spec_option:
| /* empty */ { fun t -> t }
| abs_spec    { $1 }
;

abs_spec_cv_option:
| /* empty */   { fun t -> t }
| abs_spec_cv { $1 }
;

abs_spec:
|                    tabs { $1 }
| stars                   { $1 }
| stars              tabs { fun t -> $2 ($1 t) }
| stars abs_spec_bis      { fun t -> $2 ($1 t) }
| stars abs_spec_bis tabs { fun t -> $2 ($3 ($1 t)) }
|       abs_spec_bis tabs { fun t -> $1 ($2 t) }
|       abs_spec_bis      { $1 }
;

abs_spec_cv:
|                         tabs { $1 }
| stars_cv                       { $1 }
| stars_cv                 tabs                { fun t -> $2 ($1 t) }
| stars_cv abs_spec_bis_cv       { fun t -> $2 ($1 t) }
| stars_cv abs_spec_bis_cv tabs                { fun t -> $2 ($3 ($1 t)) }
|          abs_spec_bis_cv tabs                { fun t -> $1 ($2 t) }
|          abs_spec_bis_cv       { $1 }
;

abs_spec_bis:
| LPAR abs_spec RPAR { $2 }
| abs_spec_bis LPAR abs_param_type_list RPAR { fun t -> $1 (LTarrow($3,t)) };
;

abs_spec_bis_cv:
| LPAR abs_spec_cv RPAR { $2 }
| abs_spec_bis_cv LPAR abs_param_type_list RPAR { fun t -> $1 (LTarrow($3,t)) };
;

stars:
| STAR          { fun t -> LTpointer t }
| stars STAR    { fun t -> (LTpointer ($1 t)) }
;

stars_cv:
| STAR          { fun t -> LTpointer t }
| STAR cv       { fun t -> LTattribute ((LTpointer t), $2) }
| stars_cv STAR    { fun t -> (LTpointer ($1 t)) }
| stars_cv STAR cv { fun t -> (LTattribute ((LTpointer ($1 t)), $3)) }
;

tabs:
| LSQUARE array_size RSQUARE
    {
      fun t -> LTarray (t,$2)
    }
| LSQUARE array_size RSQUARE tabs
    {
      fun t -> (LTarray ($4 t,$2))
    }
;

type_spec(tname):
| INTEGER        { LTinteger }
| REAL           { LTreal }
| BOOLEAN        { LTboolean }
| VOID           { LTvoid }
| BOOL           { LTint IBool }
| CHAR           { LTint IChar }       /** [char] */
| SIGNED CHAR    { LTint ISChar }      /** [signed char] */
| UNSIGNED CHAR  { LTint IUChar }      /** [unsigned char] */
| INT            { LTint IInt }        /** [int] */
| SIGNED INT     { LTint IInt }        /** [int] */
| UNSIGNED INT   { LTint IUInt }       /** [unsigned int] */
| UNSIGNED       { LTint IUInt }
| SHORT          { LTint IShort }      /** [short] */
| SIGNED SHORT   { LTint IShort }      /** [short] */
| UNSIGNED SHORT { LTint IUShort }     /** [unsigned short] */
| SHORT INT          { LTint IShort }      /** [short] */
| SIGNED SHORT INT   { LTint IShort }      /** [short] */
| UNSIGNED SHORT INT { LTint IUShort }     /** [unsigned short] */
| LONG           { LTint ILong }       /** [long] */
| SIGNED LONG    { LTint ILong }       /** [long] */
| UNSIGNED LONG  { LTint IULong }      /** [unsigned long] */
| SIGNED LONG INT{ LTint ILong }       /** [long] */
| LONG  INT      { LTint ILong }       /** [long] */
| UNSIGNED LONG INT { LTint IULong }      /** [unsigned long] */
| LONG LONG      { LTint ILongLong }   /** [long long] (or [_int64] on
					   Microsoft Visual C) */
| SIGNED LONG LONG   { LTint ILongLong }   /** [long long] (or [_int64] on
					   Microsoft Visual C) */
| UNSIGNED LONG LONG { LTint IULongLong }  /** [unsigned long long]
                                (or [unsigned _int64] on Microsoft Visual C) */
| LONG LONG INT     { LTint ILongLong }   /** [long long] (or [_int64] on
					   Microsoft Visual C) */
| SIGNED LONG LONG INT  { LTint ILongLong }   /** [long long] (or [_int64] on
					   Microsoft Visual C) */
| UNSIGNED LONG LONG INT { LTint IULongLong }  /** [unsigned long long]
                                (or [unsigned _int64] on Microsoft Visual C) */
| FLOAT             { LTfloat FFloat }
| DOUBLE            { LTfloat FDouble }
| LONG DOUBLE       { LTfloat FLongDouble }
| STRUCT id = identifier_or_typename_full { LTstruct id }
| ENUM id = identifier_or_typename_full { LTenum id }
| UNION id = identifier_or_typename_full  { LTunion id }
| name = tname          { LTnamed (name,[]) }
| name = tname LT prms = ne_logic_type_list(tname) GT { LTnamed(name,prms) }
;

ne_logic_type_list(tname):
| l = separated_nonempty_list(COMMA,logic_type_gen(tname)) { l }
;

symbol_identifier:
| id = full_identifier { id }
| name = LONGIDENT { name }
;

full_identifier:
| id = identifier { id }
| ADMIT { "admit" }
| ALLOCATES { "allocates" }
| ASSERT { "assert" }
| ASSIGNS { "assigns" }
| ASSUMES { "assumes" }
| AXIOM { "axiom" }
| AXIOMATIC { "axiomatic" }
| BEHAVIOR { "behavior" }
| BREAKS { "breaks" }
| CHECK { "check" }
| COMPLETE { "complete" }
| CONTINUES { "continues" }
| DECREASES { "decreases" }
| DISJOINT { "disjoint" }
| ENSURES { "ensures" }
| EXITS { "exits" }
| FREES { "frees" }
| GLOBAL { "global" }
| IMPORT { "import" }
| INDUCTIVE { "inductive" }
| INVARIANT { "invariant" }
| LEMMA { "lemma" }
| LOGIC { "logic" }
| LOOP { "loop" }
| MODEL { "model" }
| MODULE { "module" }
| PREDICATE { "predicate" }
| REQUIRES { "requires" }
| RETURNS { "returns" }
| TERMINATES { "terminates" }
| TYPE { "type" }
| VARIANT { "variant" }
| EXT_SPEC_MODULE { "module" }
| EXT_SPEC_FUNCTION { "function" }
| EXT_SPEC_CONTRACT { "contract" }
| EXT_SPEC_INCLUDE { "include" }
| EXT_SPEC_AT { "at" }
| EXT_SPEC_LET { "let" }
| id = EXT_CODE_ANNOT { fst id }
| id = EXT_CONTRACT { fst id }
| id = EXT_GLOBAL { fst id }
| id = EXT_GLOBAL_BLOCK { fst id }
| id = EXT_LOADER { fst id }
| id = EXT_LOADER_PLUGIN { fst id }
| id = IDENTIFIER_EXT { id }
| id = IDENTIFIER_LOADER { id }
;

%inline unknown_extension:
| id=IDENTIFIER_EXT content=extension_content { (id,content) }


/*** ACSL extension for external spec file ***/

ext_spec:
 | ext_global_clauses_opt ext_module_specs_opt ext_global_specs_opt EOF { (None,$1,$2)::$3 }
;

ext_global_clauses_opt:
 | /* empty */         { [] }
 | ext_global_clauses  { $1 }
;

ext_global_clauses:
| ext_global_clause                    { [$1] }
| ext_global_clause ext_global_clauses { $1::$2 }
;

ext_global_clause:
| decl  { Ext_decl (loc_decl $sloc $1) }
| GLOBAL