diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index ed1934a750d6bc7465fa4ad1f8aa9dce0e3aa9e4..0da0b7020349f1bf7f3646cddf230055b094af86 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -79,9 +79,9 @@ exception NoProto
(* Go through all the parameter names and mark them as identifiers *)
let rec findProto = function
- PROTO (d, args, _) when isJUSTBASE d ->
+ PROTO (d, args, _,_) when isJUSTBASE d ->
List.iter (fun (_, (an, _, _, _)) -> !Lexerhack.add_identifier an) args
- | PROTO (d, _, _) -> findProto d
+ | PROTO (d, _,_, _) -> findProto d
| PARENTYPE (_, d, _) -> findProto d
| PTR (_, d) -> findProto d
| ARRAY (d, _, _) -> findProto d
@@ -251,8 +251,8 @@ let transformOffsetOf (speclist, dtype) member =
ARRAY (addPointer dtype, attrs, expr)
| PTR (attrs, dtype) ->
PTR (attrs, addPointer dtype)
- | PROTO (dtype, names, variadic) ->
- PROTO (addPointer dtype, names, variadic)
+ | PROTO (dtype, names, gnames, variadic) ->
+ PROTO (addPointer dtype, names, gnames,variadic)
in
let nullType = (speclist, addPointer dtype) in
let nullExpr = mk_expr (CONSTANT (CONST_INT "0")) in
@@ -484,13 +484,13 @@ global:
let pardecl, isva = doOldParDecl $3 $5 in
(* Make the function declarator *)
doDeclaration None loc []
- [(($1, PROTO(JUSTBASE, pardecl,isva),
+ [(($1, PROTO(JUSTBASE, pardecl,[],isva),
["FC_OLDSTYLEPROTO",[]], loc), NO_INIT)]
}
| IDENT LPAREN RPAREN SEMICOLON {
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
doDeclaration None loc []
- [(($1, PROTO(JUSTBASE,[],false),
+ [(($1, PROTO(JUSTBASE,[],[],false),
["FC_OLDSTYLEPROTO",[]], loc), NO_INIT)]
}
;
@@ -524,7 +524,7 @@ postfix_expression: /*(* 6.5.2 *)*/
| primary_expression { $1 }
| postfix_expression bracket_comma_expression
{make_expr (INDEX ($1, smooth_expression $2))}
-| postfix_expression LPAREN arguments RPAREN {make_expr (CALL ($1, $3))}
+| postfix_expression LPAREN arguments RPAREN ghost_arguments_opt {make_expr (CALL ($1, $3, $5))}
| BUILTIN_VA_ARG LPAREN expression COMMA type_name RPAREN
{ let b, d = $5 in
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 5, Parsing.rhs_end_pos 5) in
@@ -534,7 +534,7 @@ postfix_expression: /*(* 6.5.2 *)*/
({ expr_loc = loc_f;
expr_node = VARIABLE "__builtin_va_arg"},
[$3; { expr_loc = loc;
- expr_node = TYPE_SIZEOF (b, d)}]))
+ expr_node = TYPE_SIZEOF (b, d)}],[]))
}
| BUILTIN_TYPES_COMPAT LPAREN type_name COMMA type_name RPAREN
{ let b1,d1 = $3 in
@@ -547,7 +547,7 @@ postfix_expression: /*(* 6.5.2 *)*/
({expr_loc = loc_f;
expr_node = VARIABLE "__builtin_types_compatible_p"},
[ { expr_loc = loc1; expr_node = TYPE_SIZEOF(b1,d1)};
- { expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}]))
+ { expr_loc = loc2; expr_node = TYPE_SIZEOF(b2,d2)}],[]))
}
| BUILTIN_OFFSETOF LPAREN type_name COMMA offsetof_member_designator RPAREN
{ transformOffsetOf $3 $5 }
@@ -795,6 +795,13 @@ gcc_init_designators: /*(* GCC supports these strange things *)*/
id_or_typename COLON { INFIELD_INIT($1, NEXT_INIT) }
;
+ghost_arguments_opt:
+ /* empty */ { [] }
+| ghost_arguments { $1 }
+
+ghost_arguments:
+ LGHOST LPAREN arguments RPAREN RGHOST { $3 }
+
arguments:
/* empty */ { [] }
| comma_expression { $1 }
@@ -1022,6 +1029,15 @@ for_clause:
| declaration { FC_DECL $1 }
;
+ghost_parameter_opt:
+ /* empty */ {[]}
+ | ghost_parameter {$1}
+;
+
+ghost_parameter:
+ LGHOST parameter_list_startscope rest_par_list RPAREN RGHOST { let (l, _) = $3 in l }
+;
+
declaration: /* ISO 6.7.*/
decl_spec_list init_declarator_list SEMICOLON
{ doDeclaration None ((snd $1)) (fst $1) $2 }
@@ -1218,14 +1234,15 @@ direct_decl: /* (* ISO 6.7.5 *) */
{ let (n, decl) = $1 in
let (attrs, size) = $3 in
(n, ARRAY(decl, attrs, size)) }
-| direct_decl LPAREN RPAREN {
- let (n,decl) = $1 in (n, PROTO(decl,[],false))
+| direct_decl LPAREN RPAREN ghost_parameter_opt {
+ let (n,decl) = $1 in (n, PROTO(decl,[],$4,false))
}
-| direct_decl parameter_list_startscope rest_par_list RPAREN
+| direct_decl parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt
{ let (n, decl) = $1 in
let (params, isva) = $3 in
+ let ghost = $5 in
!Lexerhack.pop_context ();
- (n, PROTO(decl, params, isva))
+ (n, PROTO(decl, params, ghost, isva))
}
;
parameter_list_startscope:
@@ -1266,14 +1283,14 @@ direct_old_proto_decl:
| direct_decl LPAREN old_parameter_list_ne RPAREN old_pardef_list {
let par_decl, isva = doOldParDecl $3 $5 in
let n, decl = $1 in
- (n, PROTO(decl, par_decl, isva), ["FC_OLDSTYLEPROTO",[]])
+ (n, PROTO(decl, par_decl, [],isva), ["FC_OLDSTYLEPROTO",[]])
}
/* (* appears sometimesm but generates a shift-reduce conflict. *)
| LPAREN STAR direct_decl LPAREN old_parameter_list_ne RPAREN RPAREN
LPAREN RPAREN old_pardef_list {
let par_decl, isva = doOldParDecl $5 $10 in
- let n, decl = $3 in (n, PROTO(decl, par_decl, isva), [])
+ let n, decl = $3 in (n, PROTO(decl, par_decl,[], isva), [])
}
*/
;
@@ -1336,9 +1353,9 @@ abs_direct_decl: /* (* ISO 6.7.6. We do not support optional declarator for
| abs_direct_decl parameter_list_startscope rest_par_list RPAREN
{ let (params, isva) = $3 in
!Lexerhack.pop_context ();
- PROTO ($1, params, isva)
+ PROTO ($1, params,[], isva)
}
-| abs_direct_decl LPAREN RPAREN { PROTO ($1, [], false) }
+| abs_direct_decl LPAREN RPAREN { PROTO ($1, [],[], false) }
;
abs_direct_decl_opt:
@@ -1382,11 +1399,12 @@ function_def_start: /* (* ISO 6.9.1 *) */
(snd $1, fst $1, $2)
}
/* (* New-style function that does not have a return type *) */
-| IDENT parameter_list_startscope rest_par_list RPAREN
+| IDENT parameter_list_startscope rest_par_list RPAREN ghost_parameter_opt
{ let (params, isva) = $3 in
+ let ghost = $5 in
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
let fdec =
- ($1, PROTO(JUSTBASE, params, isva), [], loc) in
+ ($1, PROTO(JUSTBASE, params, ghost, isva), [], loc) in
announceFunctionName fdec;
(* Default is int type *)
let defSpec = [SpecType Tint] in (loc, defSpec, fdec)
@@ -1398,15 +1416,15 @@ function_def_start: /* (* ISO 6.9.1 *) */
let pardecl, isva = doOldParDecl $3 $5 in
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
(* Make the function declarator *)
- let fdec = ($1, PROTO(JUSTBASE, pardecl,isva), [], loc) in
+ let fdec = ($1, PROTO(JUSTBASE, pardecl,[],isva), [], loc) in
announceFunctionName fdec;
(* Default is int type *)
(loc, [SpecType Tint], fdec)
}
-| IDENT LPAREN RPAREN
+| IDENT LPAREN RPAREN ghost_parameter_opt
{
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_start_pos 1) in
- let fdec = ($1, PROTO(JUSTBASE,[],false),[],loc) in
+ let fdec = ($1, PROTO(JUSTBASE,[],$4,false),[],loc) in
announceFunctionName fdec;
(loc, [SpecType Tint], fdec)
}
@@ -1538,20 +1556,20 @@ postfix_attr:
primary_attr { $1 }
| id_or_typename_as_id paren_attr_list_ne {
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
- make_expr (CALL({ expr_loc = loc; expr_node = VARIABLE $1}, $2)) }
+ make_expr (CALL({ expr_loc = loc; expr_node = VARIABLE $1}, $2,[])) }
/* (* use a VARIABLE "" so that the parentheses are printed *) */
| id_or_typename_as_id LPAREN RPAREN {
let loc1 = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
let loc2 = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 2, Parsing.rhs_end_pos 3) in
let f = { expr_node = VARIABLE $1; expr_loc = loc1 } in
let arg = { expr_node = VARIABLE ""; expr_loc = loc2 } in
- make_expr (CALL(f, [arg]))
+ make_expr (CALL(f, [arg],[]))
}
/* (* use a VARIABLE "" so that the parameters are printed without
* parentheses nor comma *) */
| basic_attr param_attr_list_ne {
let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 1, Parsing.rhs_end_pos 1) in
- make_expr (CALL({ expr_node = VARIABLE ""; expr_loc = loc}, $1::$2)) }
+ make_expr (CALL({ expr_node = VARIABLE ""; expr_loc = loc}, $1::$2,[])) }
| postfix_attr ARROW id_or_typename { make_expr (MEMBEROFPTR ($1, $3))}
| postfix_attr DOT id_or_typename { make_expr (MEMBEROF ($1, $3)) }
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 3137c53e5a21baab52734c1af0bbd3abc3009467..8481d90b3a09bc2957a0ecd56b8f2a4de304763d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1163,21 +1163,22 @@ end
let constFoldType (t:typ) : typ =
visitCilType constFoldTypeVisitor t
-let get_temp_name () =
+let get_temp_name ?(ghost=false) () =
let undolist = ref [] in
let data = CurrentLoc.get() in
+ let name = if ghost then "g_tmp" else "tmp" in
let name, _ =
- Alpha.newAlphaName ~alphaTable ~undolist ~lookupname:"tmp" ~data
+ Alpha.newAlphaName ~alphaTable ~undolist ~lookupname:name ~data
in
let undolist = !undolist in
Alpha.undoAlphaChanges ~alphaTable ~undolist;
name
(* Create a new temporary variable *)
-let newTempVar descr (descrpure:bool) typ =
+let newTempVar ~ghost descr (descrpure:bool) typ =
let t' = (!typeForInsertedVar) typ in
- let name = get_temp_name () in
- let vi = makeVarinfo ~temp:true false false name t' in
+ let name = get_temp_name ~ghost () in
+ let vi = makeVarinfo ~ghost ~temp:true false false name t' in
vi.vdescr <- Some descr;
vi.vdescrpure <- descrpure;
alphaConvertVarAndAddToEnv false vi
@@ -1565,7 +1566,7 @@ struct
match Cil_datatype.Varinfo.Hashtbl.find_opt replacements vi with
| None ->
let vi' =
- newTempVar (vi.vname ^ " initialization") true vi.vtype
+ newTempVar (vi.vname ^ " initialization") ~ghost true vi.vtype
in
Cil_datatype.Varinfo.Hashtbl.add replacements vi vi';
vars := vi' :: !vars;
@@ -2619,11 +2620,15 @@ let rec combineTypes (what: combineWhat) (oldt: typ) (t: typ) : typ =
let newargs, olda' =
if oldargs = None then args, olda else
if args = None then oldargs, olda else
- let oldargslist = argsToList oldargs in
- let argslist = argsToList args in
+ let (oldargslist, oldghostargslist) = argsToPairOfLists oldargs in
+ let (argslist, ghostargslist) = argsToPairOfLists args in
if List.length oldargslist <> List.length argslist then
raise (Cannot_combine "different number of arguments")
+ else if List.length oldghostargslist <> List.length ghostargslist then
+ raise (Cannot_combine "different number of ghost arguments")
else begin
+ let oldargslist = oldargslist @ oldghostargslist in
+ let argslist = argslist @ ghostargslist in
(* Construct a mapping between old and new argument names. *)
let map = H.create 5 in
List.iter2
@@ -3034,8 +3039,11 @@ let makeGlobalVarinfo (isadef: bool) (vi: varinfo) : varinfo * bool =
(try
let old_formals_env = getFormalsDecl oldvi in
List.iter2
- (fun old (name,typ,attr) ->
- if name <> "" then begin
+ (fun old ((name,typ,attr) as decl) ->
+ let new_ghost = Cil.isGhostFormalVarDecl decl in
+ if old.vghost <> new_ghost then
+ raise (Invalid_argument "Incompatible ghost status")
+ else if name <> "" then begin
Kernel.debug ~dkey:Kernel.dkey_typing_global
"replacing formal %s with %s" old.vname name;
old.vname <- name;
@@ -3961,6 +3969,8 @@ let empty_local_env =
}
let ghost_local_env ghost = {empty_local_env with is_ghost = ghost }
+let add_ghost_to_local_env env ghost =
+ { env with is_ghost = env.is_ghost || ghost }
let paren_local_env env = { env with is_paren = true }
let no_paren_local_env env = { env with is_paren = false }
@@ -4709,12 +4719,11 @@ and makeVarInfoCabs
Kernel.error ~once:true ~current:true "inline for a non-function: %s" n;
checkRestrictQualifierDeep vtype;
(* log "Looking at %s(%b): (%a)@." n isformal d_attrlist nattr;*)
- let vi = makeVarinfo ~referenced ~temp:isgenerated isglobal isformal n vtype
+ let vi = makeVarinfo ~ghost ~referenced ~temp:isgenerated isglobal isformal n vtype
in
vi.vstorage <- sto;
vi.vattr <- nattr;
vi.vdecl <- ldecl;
- vi.vghost <- ghost;
vi.vdefined <-
not (isFunctionType vtype) && isglobal && (sto = NoStorage || sto = Static);
@@ -4783,7 +4792,7 @@ and doAttr ghost (a: A.attribute) : attribute list =
end
| A.CONSTANT (A.CONST_FLOAT str) ->
ACons ("__fc_float", [AStr str])
- | A.CALL({expr_node = A.VARIABLE n}, args) -> begin
+ | A.CALL({expr_node = A.VARIABLE n}, args, []) -> begin
let n' = if strip then stripUnderscore n else n in
let ae' = List.map ae args in
ACons(n', ae')
@@ -5026,7 +5035,7 @@ and doType (ghost:bool) isFuncArg
function argument";
doDeclType (TArray(bt, lo, empty_size_cache (), al')) acc d
- | A.PROTO (d, args, isva) ->
+ | A.PROTO (d, args, ghost_args, isva) ->
(* Start a scope for the parameter names *)
enterScope ();
(* Intercept the old-style use of varargs.h. On GCC this means that
@@ -5053,9 +5062,9 @@ and doType (ghost:bool) isFuncArg
(args', !newisva)
end else (args, isva)
in
- let argl_length = List.length args' in
(* Make the argument as for a formal *)
- let doOneArg (s, (n, ndt, a, cloc)) : varinfo =
+ let doOneArg argl_length is_ghost (s, (n, ndt, a, cloc)) : varinfo =
+ let ghost = is_ghost || ghost in
let s' = doSpecList ghost n s in
let vi = makeVarInfoCabs ~ghost ~isformal:true ~isglobal:false
(convLoc cloc) s' (n,ndt,a) in
@@ -5073,13 +5082,31 @@ and doType (ghost:bool) isFuncArg
addLocalToEnv vi.vname (EnvVar vi);
vi
in
+ let make_noopt_targs ghost args =
+ let argl_length = List.length args in
+ List.map (doOneArg argl_length ghost) args
+ in
+ let noopt_targs = make_noopt_targs false args' in
+ let noopt_ghost_targs = make_noopt_targs true ghost_args in
let targs : varinfo list option =
- match List.map doOneArg args' with
+ match noopt_targs with
| [] -> None (* No argument list *)
+ | [t] when isVoidType t.vtype -> Some []
+ | l -> Some l
+ in
+ let ghost_targs : varinfo list =
+ match noopt_ghost_targs with
| [t] when isVoidType t.vtype ->
- Some []
- | l ->
- Some l
+ Kernel.error ~once:true ~current:true
+ "ghost parameters list cannot be void" ;
+ []
+ | l -> l
+ in
+ let all_targs =
+ match targs, ghost_targs with
+ | None, [] -> None
+ | None, g -> Some g
+ | Some ng, g -> Some (ng @ g)
in
exitScope ();
(* Turn [] types into pointers in the arguments and the result type.
@@ -5134,11 +5161,19 @@ and doType (ghost:bool) isFuncArg
fixupArgumentTypes (argidx + 1) args'
in
let args =
- match targs with
+ match all_targs with
| None -> None
| Some argl ->
fixupArgumentTypes 0 argl;
- Some (List.map (fun a -> (a.vname, a.vtype, a.vattr)) argl)
+ let arg_type_from_vi vi =
+ let attrs =
+ if vi.vghost then
+ cabsAddAttributes [Attr (frama_c_ghost_formal, [])] vi.vattr
+ else
+ vi.vattr
+ in (vi.vname, vi.vtype, attrs)
+ in
+ Some (List.map arg_type_from_vi argl)
in
let tres =
match unrollType bt with
@@ -5180,7 +5215,7 @@ and isVariableSizedArray ghost (dt: A.decl_type)
| PTR (al, dt) -> PTR (al, findArray dt)
| JUSTBASE -> JUSTBASE
| PARENTYPE (prea, dt, posta) -> PARENTYPE (prea, findArray dt, posta)
- | PROTO (dt, f, a) -> PROTO (findArray dt, f, a)
+ | PROTO (dt, f, g, a) -> PROTO (findArray dt, f, g, a)
in
let dt' = findArray dt in
match !res with
@@ -6034,7 +6069,7 @@ and doExp local_env
doExp local_env asconst
(cabs_exp loc
(A.CALL (cabs_exp loc (A.VARIABLE "__builtin_next_arg"),
- [cabs_exp loc (A.CONSTANT (A.CONST_INT "0"))])))
+ [cabs_exp loc (A.CONSTANT (A.CONST_INT "0"))],[])))
what
end
@@ -6141,7 +6176,7 @@ and doExp local_env
Format.asprintf "%a%s"
Cil_descriptive_printer.pp_exp e'
(if uop = A.POSINCR then "++" else "--") in
- let tmp = newTempVar descr true t in
+ let tmp = newTempVar ~ghost descr true t in
([var tmp],
local_var_chunk se' tmp +++
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
@@ -6223,7 +6258,7 @@ and doExp local_env
let descr =
Format.asprintf "%a" Cil_descriptive_printer.pp_lval lv
in
- let tmp = newTempVar descr true lvt in
+ let tmp = newTempVar ~ghost descr true lvt in
let chunk =
i2c
(mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
@@ -6345,7 +6380,7 @@ and doExp local_env
finishExp [] se e' intType
| _ ->
let tmp =
- newTempVar "<boolean expression>" true intType
+ newTempVar ~ghost "<boolean expression>" true intType
in
let condChunk =
compileCondExp ~ghost ce
@@ -6362,7 +6397,7 @@ and doExp local_env
intType
end
- | A.CALL(f, args) ->
+ | A.CALL(f, args, ghost_args) ->
let (rf,sf, f', ft') =
match (stripParen f).expr_node with
(* Treat the VARIABLE case separate because we might be calling a
@@ -6490,14 +6525,14 @@ and doExp local_env
in
let init_chunk = unspecified_chunk empty in
(* Do the arguments. In REVERSE order !!! Both GCC and MSVC do this *)
- let rec loopArgs = function
+ let rec loopArgs ?(are_ghost=false) = function
| ([], []) ->
(match argTypes, f''.enode with
| None, Lval (Var f,NoOffset) ->
(* we call a function without prototype with 0 argument.
Hence, it really has no parameter.
*)
- if not isSpecialBuiltin then begin
+ if not isSpecialBuiltin && not are_ghost then begin
warn_no_proto f;
let typ = TFun (resType, Some [], false,attrs) in
Cil.update_var_type f typ;
@@ -6510,16 +6545,18 @@ and doExp local_env
| _, [] ->
if not isSpecialBuiltin then
Kernel.error ~once:true ~current:true
- "Too few arguments in call to %a." Cil_printer.pp_exp f' ;
+ "Too few%s arguments in call to %a."
+ (if are_ghost then " ghost" else "") Cil_printer.pp_exp f' ;
(init_chunk, [])
| ((_, at, _) :: atypes, a :: args) ->
- let (ss, args') = loopArgs (atypes, args) in
+ let (ss, args') = loopArgs ~are_ghost (atypes, args) in
(* Do not cast as part of translating the argument. We let
* the castTo do this work. This was necessary for
* test/small1/union5, in which a transparent union is passed
* as an argument *)
let (sa, a', att) =
+ let local_env = add_ghost_to_local_env local_env are_ghost in
let (r, c, e, t) =
doExp (no_paren_local_env local_env) CNoConst a (AExp None)
in
@@ -6587,7 +6624,8 @@ and doExp local_env
if not isvar && argTypes != None && not isSpecialBuiltin then
(* Do not give a warning for functions without a prototype*)
Kernel.error ~once:true ~current:true
- "Too many arguments in call to %a" Cil_printer.pp_exp f';
+ "Too many%s arguments in call to %a"
+ (if are_ghost then " ghost" else "") Cil_printer.pp_exp f';
let rec loop = function
[] -> (init_chunk, [])
| a :: args ->
@@ -6636,7 +6674,18 @@ and doExp local_env
*)
)
in
- let (sargs, args') = loopArgs (argTypesList, args) in
+ let (argTypes, ghostArgTypes) =
+ List.partition (fun d -> not (isGhostFormalVarDecl d) || ghost) argTypesList
+ in
+ let args = if ghost then args @ ghost_args else args in
+
+ (* Again, we process arguments in REVERSE order. *)
+ let (sghost, ghosts') = loopArgs ~are_ghost:true (ghostArgTypes, ghost_args) in
+ let (sargs, args') = loopArgs (argTypes, args) in
+
+ let sargs = sghost @@ (sargs, false) in
+
+ let (sargs, args') = (sargs, args' @ ghosts') in
(* Setup some pointer to the elements of the call. We may change
* these below *)
let s0 = unspecified_chunk empty in
@@ -6666,9 +6715,10 @@ and doExp local_env
| _ -> e
in
(* Get the name of the last formal *)
- let getNameLastFormal () : string =
+ let getNameLastNonGhostFormal () : string =
match !currentFunctionFDEC.svar.vtype with
| TFun(_, Some args, true, _) -> begin
+ let args, _ = Cil.argsToPairOfLists (Some args) in
match List.rev args with
| (last_par_name, _, _) :: _ -> last_par_name
| _ -> ""
@@ -6688,7 +6738,7 @@ and doExp local_env
match !pwhat with
| ASet (is_real,lv, r, lvt) -> is_real, lv, r, lvt
| _ ->
- let v = newTempVar "vararg" true resTyp in
+ let v = newTempVar ~ghost "vararg" true resTyp in
locals := v::!locals;
false, var v, [], resTyp
in
@@ -6717,7 +6767,7 @@ and doExp local_env
let isOk =
match (dropCasts last).enode with
| Lval (Var lastv, NoOffset) ->
- lastv.vname = getNameLastFormal ()
+ lastv.vname = getNameLastNonGhostFormal ()
| _ -> false
in
if not isOk && variad then
@@ -6753,7 +6803,7 @@ and doExp local_env
let isOk =
match (dropCasts last).enode with
| Lval (Var lastv, NoOffset) ->
- lastv.vname = getNameLastFormal ()
+ lastv.vname = getNameLastNonGhostFormal ()
| _ -> false
in
if not isOk then
@@ -6792,7 +6842,7 @@ and doExp local_env
let isOk =
match (dropCasts last).enode with
| Lval (Var lastv, NoOffset) ->
- lastv.vname = getNameLastFormal ()
+ lastv.vname = getNameLastNonGhostFormal ()
| _ -> false
in
if not isOk then
@@ -7004,7 +7054,7 @@ and doExp local_env
Cil_descriptive_printer.pp_exp)
!pargs
in
- let tmp = newTempVar descr false restype'' in
+ let tmp = newTempVar ~ghost descr false restype'' in
tmp.vdecl <- loc;
locals:=tmp::!locals;
(* Remember that this variable has been created for this
@@ -7144,7 +7194,7 @@ and doExp local_env
let descr =
Format.asprintf "%a" Cprint.print_expression e1
in
- let tmp = newTempVar descr true tresult in
+ let tmp = newTempVar ~ghost descr true tresult in
let tmp_var = var tmp in
let tmp_lval = new_exp ~loc:e.expr_loc (Lval (tmp_var)) in
let (r1, se1, _, _) =
@@ -7213,7 +7263,7 @@ and doExp local_env
let descr =
Format.asprintf "%a" Cprint.print_expression e1
in
- let tmp = newTempVar descr true tresult in
+ let tmp = newTempVar ~ghost descr true tresult in
let tmp_var = var tmp in
let tmp_lval = new_exp ~loc:e.expr_loc (Lval (tmp_var)) in
let (r1,se1, _, _) =
@@ -7242,7 +7292,7 @@ and doExp local_env
Cil_descriptive_printer.pp_exp e2'
Cil_descriptive_printer.pp_exp e3'
in
- let tmp = newTempVar descr true tresult in
+ let tmp = newTempVar ~ghost descr true tresult in
false, var tmp, [], tresult,
local_var_chunk empty tmp
in
@@ -7315,7 +7365,7 @@ and doExp local_env
let se, e =
match se.stmts with
| [ { skind = Block b},_, _, _, _ ] ->
- let vi = newTempVar "GNU.body" true t in
+ let vi = newTempVar ~ghost "GNU.body" true t in
b.bstmts <-
b.bstmts @
[Cil.mkStmtOneInstr ~ghost:local_env.is_ghost ~valid_sid
@@ -8514,7 +8564,8 @@ and cleanup_autoreference vi chunk =
match !temp with
| Some v' -> ChangeTo v'
| None ->
- let v' = newTempVar (vi.vname ^ " initialization") true vi.vtype in
+ let ghost = v.vghost in
+ let v' = newTempVar ~ghost (vi.vname ^ " initialization") true vi.vtype in
temp := Some v';
ChangeTo v'
end else SkipChildren
@@ -8543,8 +8594,8 @@ and createLocal ghost ((_, sto, _, _) as specs)
(* Check if we are declaring a function *)
let rec isProto (dt: decl_type) : bool =
match dt with
- | PROTO (JUSTBASE, _, _) -> true
- | PROTO (x, _, _) -> isProto x
+ | PROTO (JUSTBASE, _,_, _) -> true
+ | PROTO (x, _,_, _) -> isProto x
| PARENTYPE (_, x, _) -> isProto x
| ARRAY (x, _, _) -> isProto x
| PTR (_, x) -> isProto x
@@ -8714,7 +8765,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
(* do it in two *)
let rt, _, _, _ = splitFunctionType alloca.vtype in
let tmp =
- newTempVar
+ newTempVar ~ghost
(Format.asprintf "alloca(%a)" Cil_printer.pp_exp alloca_size)
false rt
in
@@ -8776,7 +8827,7 @@ and doAliasFun vtype (thisname:string) (othername:string)
let args = List.map
(fun (n,_,_) -> { expr_loc = loc; expr_node = A.VARIABLE n})
(argsToList formals) in
- let call = A.CALL ({expr_loc = loc; expr_node = A.VARIABLE othername}, args)
+ let call = A.CALL ({expr_loc = loc; expr_node = A.VARIABLE othername}, args,[])
in
let stmt = {stmt_ghost = false;
stmt_node = if isVoidType rt then
@@ -8983,8 +9034,9 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
(* Create the formals and add them to the environment. *)
(* sfg: extract tsets for the formals from dt *)
- let doFormal (loc : location) (fn, ft, fa) =
- let f = makeVarinfo ~temp:false false true fn ft in
+ let doFormal (loc : location) ((fn, ft, fa) as fd) =
+ let ghost = ghost || isGhostFormalVarDecl fd in
+ let f = makeVarinfo ~ghost ~temp:false false true fn ft in
(f.vdecl <- loc;
f.vattr <- fa;
alphaConvertVarAndAddToEnv true f)
@@ -9005,7 +9057,7 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function
f' :: fl'
end
in
- let fmlocs = (match dt with PROTO(_, fml, _) -> fml | _ -> []) in
+ let fmlocs = (match dt with PROTO(_, fml, _, _) -> fml | _ -> []) in
let formals = doFormals (argsToList formals_t) fmlocs in
(* in case of formals referred to in types of others, doType has
put dummy varinfos. We need to fix them now that we have proper
diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml
index d4d4103964a90292cadc12908ab670513e9f0b7a..2bc549d5caf779a1dcc81ebca20143fe31af2de7 100644
--- a/src/kernel_internals/typing/infer_annotations.ml
+++ b/src/kernel_internals/typing/infer_annotations.ml
@@ -56,14 +56,14 @@ let assigns_from_prototype kf =
if Cil.isVoidPtrType typ then
let const = typeHasAttribute "const" (Cil.typeOf_pointed typ) in
let typ' = if const then Cil.charConstPtrType else Cil.charPtrType in
- (Logic_utils.mk_cast ~loc typ' t, typ')
- else (t, typ)
+ (vi.vghost, Logic_utils.mk_cast ~loc typ' t, typ')
+ else (vi.vghost, t, typ)
) pointer_args
in
(* Generate the term [*(t+(0..))] with the appropriate array bounds (if
they are known), and possibly add some [[..]] if v has points to one or
more arrays *)
- let mk_star (t, typ) =
+ let mk_star (g, t, typ) =
let loc = t.term_loc in
let zero = Logic_const.tinteger ~loc 0 in
(* Range [0..length-1], or [0..] if length is not known *)
@@ -108,14 +108,16 @@ let assigns_from_prototype kf =
let t_range =
Logic_const.term ~loc t_range_node (if set then make_set_type (Ctype typ) else Ctype typ)
in
- Logic_const.new_identified_term
- (term ~loc (TLval (TMem t_range, offset_arrays)) typ_with_offset)
+ let t = Logic_const.new_identified_term
+ (term ~loc (TLval (TMem t_range, offset_arrays)) typ_with_offset)
+ in
+ (g, t)
in
let to_assign =
List.map
mk_star
(List.filter
- (fun (_t, typ) ->
+ (fun (_g, _t, typ) ->
let pointed_type = typeOf_pointed typ in
not (typeHasAttribute "const" pointed_type)
)
@@ -125,28 +127,35 @@ let assigns_from_prototype kf =
List.map mk_star pointer_args
in
let inputs =
- (pointer_args_content
- @(List.map
- (fun v ->
- Logic_const.new_identified_term
- { term_node = TLval (TVar (cvar_to_lvar v),TNoOffset);
- term_type = Ctype v.vtype;
- term_name = [];
- term_loc = v.vdecl })
- basic_args))
+ (pointer_args_content)
+ @(List.map
+ (fun v ->
+ v.vghost,
+ (Logic_const.new_identified_term
+ { term_node = TLval (TVar (cvar_to_lvar v),TNoOffset);
+ term_type = Ctype v.vtype;
+ term_name = [];
+ term_loc = v.vdecl })
+ ) basic_args)
+ in
+ let inputs_no_ghost = List.fold_right
+ (fun (g, t) acc -> if g then acc else t :: acc) inputs []
in
+ let inputs = List.map (fun (_g, t) -> t) inputs in
let arguments =
- List.map (fun content -> content, From inputs) to_assign
+ List.map
+ (fun (g, content) -> content, From (if g then inputs else inputs_no_ghost))
+ to_assign
in
match rtyp with
| TVoid _ ->
(* assigns all pointer args from basic args and content of pointer args *)
- arguments
+ arguments
| _ ->
(* assigns result from basic args and content of pointer args *)
let loc = vi.vdecl in
let result = Logic_const.(new_identified_term (tresult ~loc rtyp)) in
- (result, From inputs):: arguments
+ (result, From inputs_no_ghost):: arguments
let is_frama_c_builtin name =
Ast_info.is_frama_c_builtin name
diff --git a/src/kernel_services/ast_printing/cabs_debug.ml b/src/kernel_services/ast_printing/cabs_debug.ml
index fc191d8582406f56fdf3e527c994494655181a0d..b5880e1ae7e042ebf564682ae3e75c35da0f8aed 100644
--- a/src/kernel_services/ast_printing/cabs_debug.ml
+++ b/src/kernel_services/ast_printing/cabs_debug.ml
@@ -117,9 +117,9 @@ and pp_decl_type fmt = function
| ARRAY (decl_type, attrs, exp)
-> fprintf fmt "@[<hov 2>ARRAY[%a, %a, %a]@]" pp_decl_type decl_type pp_attrs attrs pp_exp exp
| PTR (attrs, decl_type) -> fprintf fmt "@[<hov 2>PTR(%a, %a)@]" pp_attrs attrs pp_decl_type decl_type
- | PROTO (decl_type, single_names, b)
+ | PROTO (decl_type, single_names, single_ghost_names, b)
-> fprintf fmt "@[<hov 2>PROTO decl_type(%a), single_names(" pp_decl_type decl_type;
- List.iter (fun sn -> fprintf fmt ",@ %a" pp_single_name sn) single_names;
+ List.iter (fun sn -> fprintf fmt ",@ %a" pp_single_name sn) (single_names @ single_ghost_names) ;
fprintf fmt "),@ %b@]" b
and pp_name_group fmt (spec, names) =
@@ -329,11 +329,11 @@ and pp_exp_node fmt = function
fprintf fmt "@[<hov 2>QUESTION(%a, %a, %a)@]" pp_exp exp1 pp_exp exp2 pp_exp exp3
| CAST ((spec, decl_type), init_exp) ->
fprintf fmt "@[<hov 2>CAST (%a, %a) %a@]" pp_spec spec pp_decl_type decl_type pp_init_exp init_exp
- | CALL (exp1, exps) ->
+ | CALL (exp1, exps, ghosts) ->
fprintf fmt "@[<hov 2>CALL %a {" pp_exp exp1;
List.iter
(fun e -> fprintf fmt ",@ %a" pp_exp e)
- exps;
+ (exps @ ghosts);
fprintf fmt "}@]"
| COMMA exps ->
fprintf fmt "@[<hov 2>COMMA {";
diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml
index adc133983a5b15ff4fa3ea4afa4266fd2d5e5b23..13259d5a56cf1cbc129ac1842053fbaf8d629cec 100644
--- a/src/kernel_services/ast_printing/cil_printer.ml
+++ b/src/kernel_services/ast_printing/cil_printer.ml
@@ -65,6 +65,7 @@ let register_shallow_attribute s =
reserved_attributes:=
(Extlib.strip_underscore s)::!reserved_attributes
+let () = register_shallow_attribute Cil.frama_c_ghost_formal
let () = register_shallow_attribute Cil.frama_c_mutable
let () = register_shallow_attribute Cil.frama_c_init_obj
@@ -871,10 +872,35 @@ class cil_printer () = object (self)
(match e.enode with
| Lval(Var _, _) -> self#exp fmt e
| _ -> fprintf fmt "(%a)" self#exp e);
+
+ let (_, param_ts, _, _) = Cil.splitFunctionType (Cil.typeOf e) in
+ let _, g_params_ts = Cil.argsToPairOfLists param_ts in
+
+ let rec break n l =
+ if n = 0 then [], l
+ else match l with
+ | [] -> assert false
+ | x :: l' -> let (f, s) = break (n-1) l' in x :: f, s
+ in
+ let args, ghosts = if is_ghost then
+ args, []
+ else
+ let n = List.length args - List.length g_params_ts in
+ break n args
+ in
+
(* Now the arguments *)
+ Format.fprintf fmt "@[" ;
Pretty_utils.pp_flowlist ~left:"(" ~sep:"," ~right:")" self#exp fmt args;
+ (* Now the ghost arguments *)
+ begin match ghosts with
+ | [] -> ()
+ | _ -> Pretty_utils.pp_flowlist
+ ~left:"@;/*@@ ghost (" ~sep:"," ~right:") */"
+ self#exp fmt ghosts
+ end ;
(* Now the terminator *)
- fprintf fmt "%s" instr_terminator
+ fprintf fmt "@]%s" instr_terminator
in
match i with
| Skip _ -> fprintf fmt ";"
@@ -1881,8 +1907,19 @@ class cil_printer () = object (self)
else if nameOpt = None then printAttributes fmt a
else fprintf fmt "(%a%a)" printAttributes a pname (a <> [])
in
- let pp_params fmt args pp_args =
- fprintf fmt "%t(@[%t@])" name'
+ let partition_ghosts ghost_arg args =
+ match args with
+ | None -> None, []
+ | Some l ->
+ let ghost_args, args = if is_ghost then
+ [], l
+ else
+ List.partition ghost_arg l
+ in
+ Some args, ghost_args
+ in
+ let pp_params fmt (args, ghost_args) pp_args =
+ fprintf fmt "%t@[<hv>(@[%t@])%t@]" name'
(fun fmt ->
match args with
| (None | Some []) when isvararg -> fprintf fmt "..."
@@ -1891,6 +1928,9 @@ class cil_printer () = object (self)
| Some args ->
Pretty_utils.pp_list ~sep:",@ " pp_args fmt args;
if isvararg then fprintf fmt "@ , ...")
+ (fun fmt ->
+ Pretty_utils.pp_list ~pre:"@;/*@@ ghost (@[" ~suf:"@]) */" ~sep:",@ "
+ pp_args fmt ghost_args)
in
let pp_params fmt = match fundecl with
| None ->
@@ -1902,12 +1942,14 @@ class cil_printer () = object (self)
(self#typ (Some (fun fmt -> fprintf fmt "%s" aname))) atype
self#attributes rest
in
- pp_params fmt args pp_args
+ let p = partition_ghosts Cil.isGhostFormalVarDecl args in
+ pp_params fmt p pp_args
| Some fundecl ->
let args =
try Some (Cil.getFormalsDecl fundecl) with Not_found -> None
in
- pp_params fmt args self#vdecl
+ let p = partition_ghosts Cil.isGhostFormalVarinfo args in
+ pp_params fmt p self#vdecl
in
self#typ (Some pp_params) fmt restyp
diff --git a/src/kernel_services/ast_printing/cprint.ml b/src/kernel_services/ast_printing/cprint.ml
index f8169bee15b726553ec0274ce89dfc58465824fd..36b2a4797aae3cf09a6df313fa153a663d157dac 100644
--- a/src/kernel_services/ast_printing/cprint.ml
+++ b/src/kernel_services/ast_printing/cprint.ml
@@ -251,9 +251,9 @@ and print_decl (n: string) fmt = function
| ARRAY (d, al, e) ->
fprintf fmt "%a[@[%a%a@]]"
(print_decl n) d print_attributes al print_expression e
- | PROTO(d, args, isva) ->
- fprintf fmt "@[%a@;(%a)@]"
- (print_decl n) d print_params (args,isva)
+ | PROTO(d, args, ghost_args, isva) ->
+ fprintf fmt "@[%a@;(%a) /*@@@ ghost (%a) */ @]"
+ (print_decl n) d print_params (args,isva) print_params (ghost_args, false)
and print_fields fmt (flds : field_group list) =
pp_list ~sep:"@ " print_field_group fmt flds
@@ -366,12 +366,12 @@ and print_expression_level (lvl: int) fmt (exp : expression) =
fprintf fmt "(@[%a@])@;%a"
print_onlytype typ print_cast_expression iexp
| CALL ({ expr_node = VARIABLE "__builtin_va_arg"},
- [arg; { expr_node = TYPE_SIZEOF (bt, dt) } ]) ->
+ [arg; { expr_node = TYPE_SIZEOF (bt, dt) } ], _) ->
fprintf fmt "__builtin_va_arg(@[%a,@ %a@])"
(print_expression_level 0) arg print_onlytype (bt, dt)
- | CALL (exp, args) ->
- fprintf fmt "%a(@[@;%a@])"
- print_expression exp print_comma_exps args
+ | CALL (exp, args, ghost_args) ->
+ fprintf fmt "%a(@[@;%a@]) /*@@@ ghost (@[@;%a@]) */"
+ print_expression exp print_comma_exps args print_comma_exps ghost_args
| CONSTANT (CONST_INT i) -> pp_print_string fmt i
| CONSTANT (CONST_FLOAT f) -> pp_print_string fmt f
| CONSTANT (CONST_CHAR c) -> fprintf fmt "'%s'" (escape_wstring c)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index ef22afcb87bfa37c7133f9e6fdfc8bc8e5ccc7bf..d0c3ac7a37378cb563dcb907b26abac3bb43ced6 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -302,6 +302,16 @@ let stmt_of_instr_list ?(loc=Location.unknown) = function
(**** ATTRIBUTES ****)
+(* Attributes are added as they are (e.g. if we add ["__attr"] and then ["attr"] both are added).
+ When checking for the presence of an attribute [x] or trying to remove it, underscores are
+ removed at the beginning and the end of the attribute for both the [x] attribute and the
+ attributes of the list. For example, if have a call:
+
+ dropAttribute "__const" [ Attr("const", []) ; Attr("__const", []) ; Attr("__const__", []) ]
+
+ The result is [].
+*)
+
let bitfield_attribute_name = "FRAMA_C_BITFIELD_SIZE"
(** Construct sorted lists of attributes ***)
@@ -326,11 +336,12 @@ let addAttributes al0 (al: attributes) : attributes =
List.fold_left (fun acc a -> addAttribute a acc) al al0
let dropAttribute (an: string) (al: attributes) =
+ let an = Extlib.strip_underscore an in
List.filter (fun a -> attributeName a <> an) al
-let hasAttribute (s: string) (al: attribute list) : bool =
- let s = Extlib.strip_underscore s in
- List.exists (fun a -> attributeName a = s) al
+let hasAttribute (an: string) (al: attribute list) : bool =
+ let an = Extlib.strip_underscore an in
+ List.exists (fun a -> attributeName a = an) al
let rec dropAttributes (anl: string list) (al: attributes) =
match al with
@@ -342,13 +353,15 @@ let rec dropAttributes (anl: string list) (al: attributes) =
else
if q' == q then al (* preserve sharing *) else a :: q'
-let filterAttributes (s: string) (al: attribute list) : attribute list =
- List.filter (fun a -> attributeName a = s) al
+let filterAttributes (an: string) (al: attribute list) : attribute list =
+ let an = Extlib.strip_underscore an in
+ List.filter (fun a -> attributeName a = an) al
-let findAttribute (s: string) (al: attribute list) : attrparam list =
+let findAttribute (an: string) (al: attribute list) : attrparam list =
+ let an = Extlib.strip_underscore an in
List.fold_left
(fun acc -> function
- | Attr (an, param) when an = s -> param @ acc
+ | Attr (_, param) as a0 when attributeName a0 = an -> param @ acc
| _ -> acc)
[] al
@@ -555,6 +568,20 @@ let partitionAttributes
in
loop ([], [], []) attrs
+let frama_c_ghost_formal = "__fc_ghost_formal"
+let () = registerAttribute frama_c_ghost_formal (AttrName false)
+let () =
+ registerAttribute (Extlib.strip_underscore frama_c_ghost_formal) (AttrName false)
+
+let frama_c_mutable = "__fc_mutable"
+let () = registerAttribute frama_c_mutable (AttrName false)
+let () =
+ registerAttribute (Extlib.strip_underscore frama_c_mutable) (AttrName false)
+
+let frama_c_init_obj = "__fc_initialized_object"
+let () = registerAttribute frama_c_init_obj (AttrName false)
+let () =
+ registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
let unrollType (t: typ) : typ =
let rec withAttrs (al: attributes) (t: typ) : typ =
@@ -573,7 +600,10 @@ let rec unrollTypeSkel = function
| x -> x
(* Make a varinfo. Used mostly as a helper function below *)
-let makeVarinfo ?(source=true) ?(temp=false) ?(referenced=false) global formal name typ =
+let makeVarinfo
+ ?(source=true) ?(temp=false) ?(referenced=false) ?(ghost=false)
+ global formal name typ
+ =
let vi =
{ vorig_name = name;
vname = name;
@@ -591,7 +621,7 @@ let makeVarinfo ?(source=true) ?(temp=false) ?(referenced=false) global formal n
vreferenced = referenced;
vdescr = None;
vdescrpure = true;
- vghost = false;
+ vghost = ghost;
vsource = source;
vlogic_var_assoc = None
}
@@ -612,14 +642,22 @@ module FormalsDecl =
let selfFormalsDecl = FormalsDecl.self
let () = dependency_on_ast selfFormalsDecl
-let makeFormalsVarDecl (n,t,a) =
- let vi = makeVarinfo ~temp:false false true n t in
+let makeFormalsVarDecl ?ghost (n,t,a) =
+ let vi = makeVarinfo ?ghost ~temp:false false true n t in
vi.vattr <- a;
vi
+let isGhostFormalVarinfo vi =
+ hasAttribute frama_c_ghost_formal vi.vattr
+
+let isGhostFormalVarDecl (_name, _type, attr) =
+ hasAttribute frama_c_ghost_formal attr
+
let setFormalsDecl vi typ =
match unrollType typ with
| TFun(_, Some args, _, _) ->
+ let is_ghost d = vi.vghost || isGhostFormalVarDecl d in
+ let makeFormalsVarDecl x = makeFormalsVarDecl ~ghost:(is_ghost x) x in
FormalsDecl.replace vi (List.map makeFormalsVarDecl args)
| TFun(_,None,_,_) -> ()
| _ ->
@@ -3509,17 +3547,6 @@ let typeOf_array_elem t =
| TArray (ty_elem, _, _, _) -> ty_elem
| _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
-
-let frama_c_mutable = "__fc_mutable"
-let () = registerAttribute frama_c_mutable (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_mutable) (AttrName false)
-
-let frama_c_init_obj = "__fc_initialized_object"
-let () = registerAttribute frama_c_init_obj (AttrName false)
-let () =
- registerAttribute (Extlib.strip_underscore frama_c_init_obj) (AttrName false)
-
let no_op_coerce typ t =
match typ with
| Lreal -> true
@@ -5201,11 +5228,11 @@ let rec findUniqueName ?(suffix="") fdec name =
let refresh_local_name fdec vi =
let new_name = findUniqueName fdec vi.vname in vi.vname <- new_name
-let makeLocal ?(temp=false) ?referenced ?(formal=false) fdec name typ =
+let makeLocal ?(temp=false) ?referenced ?ghost ?(formal=false) fdec name typ =
(* a helper function *)
let name = findUniqueName fdec name in
fdec.smaxid <- 1 + fdec.smaxid;
- let vi = makeVarinfo ~temp ?referenced false formal name typ in
+ let vi = makeVarinfo ~temp ?referenced ?ghost false formal name typ in
vi
(* Make a local variable and add it to a function *)
@@ -5275,21 +5302,35 @@ let setMaxId (f: fundec) =
* this one. If where = "^" then it is inserted first. If where = "$" then
* it is inserted last. Otherwise where must be the name of a formal after
* which to insert this. By default it is inserted at the end. *)
-let makeFormalVar fdec ?(where = "$") name typ : varinfo =
+let makeFormalVar fdec ?(ghost=fdec.svar.vghost) ?(where = "$") name typ : varinfo =
+ assert ((not fdec.svar.vghost) || ghost) ;
+ let makeit name =
+ let vi = makeLocal ~ghost ~formal:true fdec name typ in
+ if ghost && not fdec.svar.vghost then
+ vi.vattr <- addAttribute (Attr(frama_c_ghost_formal, [])) vi.vattr ;
+ vi
+ in
+ let error () = Kernel.fatal ~current:true
+ "makeFormalVar: cannot find insert-after formal %s" where
+ in
(* Search for the insertion place *)
- let makeit name = makeLocal ~formal:true fdec name typ in
let rec loopFormals acc = function
- [] ->
+ | [] ->
+ if where = "$" || (ghost && where = "^") then
+ let vi = makeit name in vi, List.rev (vi :: acc)
+ else error ()
+ | f :: rest when not ghost && f.vghost ->
if where = "$" then
- let vi = makeit name in vi, List.rev (vi::acc)
- else Kernel.fatal ~current:true
- "makeFormalVar: cannot find insert-after formal %s" where
- | f :: rest when f.vname = where ->
+ let vi = makeit name in vi, List.rev_append acc (vi :: f :: rest)
+ else error ()
+ | f :: rest when f.vname = where && f.vghost = ghost ->
let vi = makeit name in vi, List.rev_append acc (f :: vi :: rest)
+ | f :: rest when ghost && f.vghost && where = "^" ->
+ let vi = makeit name in vi, List.rev_append acc (vi :: f :: rest)
| f :: rest -> loopFormals (f::acc) rest
in
let vi, newformals =
- if where = "^" then let vi = makeit name in vi, vi :: fdec.sformals
+ if where = "^" && not ghost then let vi = makeit name in vi, vi :: fdec.sformals
else
loopFormals [] fdec.sformals
in
@@ -5793,6 +5834,11 @@ let splitFunctionTypeVI (fvi: varinfo)
TFun (rt, args, isva, a) -> rt, args, isva, a
| _ -> Kernel.abort "Function %s invoked on a non function type" fvi.vname
+let argsToPairOfLists args =
+ List.partition
+ (fun f -> not(isGhostFormalVarDecl f))
+ (argsToList args)
+
let remove_attributes_for_integral_promotion a =
dropAttributes (bitfield_attribute_name :: spare_attributes_for_c_cast) a
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2c60334fc5ed4d032a1d2c3e885049b7ae99a9d2..ac0127f5508893459f4947bb479043bdddf631c1 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -180,8 +180,11 @@ val setMaxId: fundec -> unit
val selfFormalsDecl: State.t
(** state of the table associating formals to each prototype. *)
-val makeFormalsVarDecl: (string * typ * attributes) -> varinfo
- (** creates a new varinfo for the parameter of a prototype. *)
+val makeFormalsVarDecl: ?ghost:bool -> (string * typ * attributes) -> varinfo
+ (** creates a new varinfo for the parameter of a prototype.
+ By default, this formal variable is not ghost.
+ @modify 19.0-Potassium+dev adds a parameter for ghost status
+ *)
(** Update the formals of a function declaration from its identifier and its
type. For a function definition, use {!Cil.setFormals}.
@@ -580,10 +583,17 @@ val isTypeTagType: logic_type -> bool
@since Nitrogen-20111001 moved from cabs2cil *)
val isVariadicListType: typ -> bool
-(** Obtain the argument list ([] if None) *)
+(** Obtain the argument list ([] if None).
+ @since 19.0-Potassium+dev Beware that it contains the ghost arguments. *)
val argsToList:
(string * typ * attributes) list option -> (string * typ * attributes) list
+(** @since 19.0-Potassium+dev
+ Obtain the argument lists (non-ghost, ghosts) ([], [] if None) *)
+val argsToPairOfLists:
+ (string * typ * attributes) list option ->
+ (string * typ * attributes) list * (string * typ * attributes) list
+
(** True if the argument is an array type *)
val isArrayType: typ -> bool
@@ -648,19 +658,33 @@ val splitFunctionTypeVI:
[vsource] .
The [referenced] argument defaults to [false], and corresponds to the field
[vreferenced] .
+ The [ghost] argument defaults to [false], and corresponds to the field
+ [vghost] .
The first unnamed argument specifies whether the varinfo is for a global and
- the second is for formals. *)
+ the second is for formals.
+ @modify 19.0-Potassium adds an optional ghost parameter
+*)
val makeVarinfo:
- ?source:bool -> ?temp:bool -> ?referenced:bool -> bool -> bool -> string ->
- typ -> varinfo
+ ?source:bool -> ?temp:bool -> ?referenced:bool -> ?ghost:bool -> bool -> bool
+ -> string -> typ -> varinfo
(** Make a formal variable for a function declaration. Insert it in both the
sformals and the type of the function. You can optionally specify where to
insert this one. If where = "^" then it is inserted first. If where = "$"
then it is inserted last. Otherwise where must be the name of a formal
after which to insert this. By default it is inserted at the end.
+
+ The [ghost] parameter indicates if the variable should be inserted in the
+ list of formals or ghost formals. By default, it takes the ghost status of
+ the function where the formal is inserted. Note that:
+
+ - specifying ghost to false if the function is ghost leads to an error
+ - when [where] is specified, its status must be the same as the formal to
+ insert (else, it cannot be found in the list of ghost or non ghost formals)
+
+ @modify 19.0-Potassium adds the optional ghost parameter
*)
-val makeFormalVar: fundec -> ?where:string -> string -> typ -> varinfo
+val makeFormalVar: fundec -> ?ghost:bool -> ?where:string -> string -> typ -> varinfo
(** Make a local variable and add it to a function's slocals and to the given
block (only if insert = true, which is the default).
@@ -1171,6 +1195,12 @@ val dropAttribute: string -> attributes -> attributes
* Maintains the attributes in sorted order *)
val dropAttributes: string list -> attributes -> attributes
+(** A varinfo marked with this attribute is known to be a ghost formal.
+
+ @since 19.0-Potassium+dev
+*)
+val frama_c_ghost_formal: string
+
(** a field struct marked with this attribute is known to be mutable, i.e.
it can be modified even on a const object.
@@ -1191,6 +1221,18 @@ val frama_c_init_obj: string
*)
val is_mutable_or_initialized: lval -> bool
+(** [true] if the given varinfo is a ghost formal variable.
+
+ @since 19.0-Potassium+dev
+*)
+val isGhostFormalVarinfo: varinfo -> bool
+
+(** [true] if the given formal declaration corresponds to a ghost formal variable.
+
+ @since 19.0-Potassium+dev
+*)
+val isGhostFormalVarDecl: (string * typ * attributes) -> bool
+
(** Remove attributes whose name appears in the first argument that are
present anywhere in the fully expanded version of the type.
@since Oxygen-20120901
diff --git a/src/kernel_services/parsetree/cabs.ml b/src/kernel_services/parsetree/cabs.ml
index 8bd397788c5cbdbfe152a59cd224cf720b233e59..462f4edd55adad2feecc6fb1b61de3ddd09ed363 100644
--- a/src/kernel_services/parsetree/cabs.ml
+++ b/src/kernel_services/parsetree/cabs.ml
@@ -121,7 +121,7 @@ and decl_type =
(* Prints "decl [ attrs exp ]".
* decl is never a PTR. *)
| PTR of attribute list * decl_type (* Prints "* attrs decl" *)
- | PROTO of decl_type * single_name list * bool
+ | PROTO of decl_type * single_name list * single_name list * bool
(* Prints "decl (args[, ...])".
* decl is never a PTR.*)
@@ -299,7 +299,7 @@ and cabsexp =
(* There is a special form of CALL in which the function called is
__builtin_va_arg and the second argument is sizeof(T). This
should be printed as just T *)
- | CALL of expression * expression list
+ | CALL of expression * expression list * expression list
| COMMA of expression list
| CONSTANT of constant
| PAREN of expression
diff --git a/src/kernel_services/visitors/cabsvisit.ml b/src/kernel_services/visitors/cabsvisit.ml
index d07ddf97c3ecd54d9b6e83be99c9f85a602ae1ba..2237d0abe0a4a9b6e410c3f699d96613d437dc9d 100644
--- a/src/kernel_services/visitors/cabsvisit.ml
+++ b/src/kernel_services/visitors/cabsvisit.ml
@@ -193,14 +193,17 @@ and childrenDeclType isfundef vis dt =
let al' = mapNoCopy (childrenAttribute vis) al in
let dt1' = visitCabsDeclType vis isfundef dt1 in
if al' != al || dt1' != dt1 then PTR(al', dt1') else dt
- | PROTO (dt1, snl, b) ->
+ | PROTO (dt1, snl, gsnl, b) ->
(* Do not propagate isfundef further *)
let dt1' = visitCabsDeclType vis false dt1 in
let _ = vis#vEnterScope () in
let snl' = mapNoCopy (childrenSingleName vis NVar) snl in
+ let gsnl' = mapNoCopy (childrenSingleName vis NVar) gsnl in
(* Exit the scope only if not in a function definition *)
let _ = if not isfundef then vis#vExitScope () in
- if dt1' != dt1 || snl' != snl then PROTO(dt1', snl', b) else dt
+ if dt1' != dt1 || snl' != snl || gsnl' != gsnl then
+ PROTO(dt1', snl', gsnl' , b)
+ else dt
and childrenNameGroup vis (kind: nameKind) ((s, nl) as input) =
@@ -430,11 +433,12 @@ and childrenExpression vis e =
let ie' = visitCabsInitExpression vis ie in
if s' != s || dt' != dt || ie' != ie then
{ e with expr_node = CAST ((s', dt'), ie')} else e
- | CALL (f, el) ->
+ | CALL (f, el, gl) ->
let f' = ve f in
let el' = mapNoCopy ve el in
+ let gl' = mapNoCopy ve gl in
if f' != f || el' != el then
- { e with expr_node = CALL (f', el')} else e
+ { e with expr_node = CALL (f', el',gl')} else e
| COMMA el ->
let el' = mapNoCopy ve el in
if el' != el then { e with expr_node = COMMA (el') } else e
diff --git a/src/plugins/variadic/extends.ml b/src/plugins/variadic/extends.ml
index 3b796f36c97be94451b34b454527c86ec004f633..c838e0a5b4a0b1aa44070f36a322129e79274d40 100644
--- a/src/plugins/variadic/extends.ml
+++ b/src/plugins/variadic/extends.ml
@@ -35,6 +35,11 @@ module Typ = struct
| TFun (_,args,_,_) -> Cil.argsToList args
| _ -> invalid_arg "params"
+ let ghost_partitioned_params typ =
+ match Cil.unrollType typ with
+ | TFun (_,args,_,_) -> Cil.argsToPairOfLists args
+ | _ -> invalid_arg "params"
+
let params_types typ =
List.map (fun (_,typ,_) -> typ) (params typ)
diff --git a/src/plugins/variadic/extends.mli b/src/plugins/variadic/extends.mli
index 93f8e685daabc9cd856d1c19942679921ba8803f..916c7322a4b20634c4b64fa8294f03b7c01a9b9f 100644
--- a/src/plugins/variadic/extends.mli
+++ b/src/plugins/variadic/extends.mli
@@ -25,6 +25,9 @@ open Cil_types
module Typ : sig
val attributes_less_equal : typ -> typ -> bool
val params : typ -> (string * typ * attributes) list
+ val ghost_partitioned_params : typ ->
+ (string * typ * attributes) list *
+ (string * typ * attributes) list
val params_types : typ -> typ list
val params_count : typ -> int
val is_variadic : typ -> bool
diff --git a/src/plugins/variadic/generic.ml b/src/plugins/variadic/generic.ml
index ace7d6b5d8b31e3f93c60628c24609cec8fff14d..af1f6658b94062ea666141de0224163252757e8b 100644
--- a/src/plugins/variadic/generic.ml
+++ b/src/plugins/variadic/generic.ml
@@ -42,7 +42,9 @@ let translate_type = function
| TFun (ret_typ, args, is_variadic, attributes) ->
let new_args =
if is_variadic
- then Some (Cil.argsToList args @ [vpar])
+ then
+ let ng_args, g_args = Cil.argsToPairOfLists args in
+ Some (ng_args @ [vpar] @ g_args)
else args
in
TFun (ret_typ, new_args, false, attributes)
@@ -141,9 +143,12 @@ let translate_call ~fundec block loc mk_call callee pars =
Self.result ~current:true ~level:2
"Generic translation of call to variadic function.";
- (* Split params into static and variadic part *)
- let static_size = List.length (Typ.params (Cil.typeOf callee)) - 1 in
- let s_exps, v_exps = List.break static_size pars in
+ (* Split params into static, variadic and ghost part *)
+ let ng_params, g_params = Typ.ghost_partitioned_params (Cil.typeOf callee) in
+ let static_size = List.length ng_params - 1 in
+ let s_exps, r_exps = List.break static_size pars in
+ let variadic_size = (List.length r_exps) - (List.length g_params) in
+ let v_exps, g_exps = List.break variadic_size r_exps in
(* Create temporary variables to hold parameters *)
let add_var i exp =
@@ -168,6 +173,6 @@ let translate_call ~fundec block loc mk_call callee pars =
(* Translate the call *)
let exp_vargs = Cil.mkAddrOrStartOf ~loc (Cil.var vargs) in
let new_arg = Cil.mkCast ~force:false ~e:exp_vargs ~newt:(vpar_typ []) in
- let new_args = s_exps @ [new_arg] in
+ let new_args = s_exps @ [new_arg] @ g_exps in
let call = mk_call callee new_args in
instrs @ [call]
diff --git a/src/plugins/variadic/tests/declared/empty-vpar-with-ghost.i b/src/plugins/variadic/tests/declared/empty-vpar-with-ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..58133079e349be5c8510d3f9d16aa333af62719c
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/empty-vpar-with-ghost.i
@@ -0,0 +1,10 @@
+/*@ behavior bhv:
+ @ requires c>0;
+ @ requires a<=42;
+*/
+void f(const int a, int, int c,...) /*@ ghost(int x) */;
+
+int main(){
+ f(1, 2, 3) /*@ ghost(4) */;
+ return 0;
+}
diff --git a/src/plugins/variadic/tests/declared/empty-vpar.c b/src/plugins/variadic/tests/declared/empty-vpar.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/empty-vpar.c
rename to src/plugins/variadic/tests/declared/empty-vpar.i
diff --git a/src/plugins/variadic/tests/declared/function-ptr-with-ghost.i b/src/plugins/variadic/tests/declared/function-ptr-with-ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..0ab1f1a1c0c7e5597794b56a0192ee6cb5cf9206
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/function-ptr-with-ghost.i
@@ -0,0 +1,8 @@
+void function(void (*p) (int, ...) /*@ ghost (int v) */, int x){
+ (*p) (x, 1, 2, 3) /*@ ghost (4) */;
+}
+void va_f(int, ...) /*@ ghost(int x) */ ;
+
+int main(void){
+ function(va_f, 3);
+}
\ No newline at end of file
diff --git a/src/plugins/variadic/tests/declared/label.c b/src/plugins/variadic/tests/declared/label.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/label.c
rename to src/plugins/variadic/tests/declared/label.i
diff --git a/src/plugins/variadic/tests/declared/multi.c b/src/plugins/variadic/tests/declared/multi.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/multi.c
rename to src/plugins/variadic/tests/declared/multi.i
diff --git a/src/plugins/variadic/tests/declared/no-va-with-ghost.i b/src/plugins/variadic/tests/declared/no-va-with-ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..695904970b910b711d2c199fcfb88874a50e6fc8
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/no-va-with-ghost.i
@@ -0,0 +1,5 @@
+int f(int a, int b, int c) /*@ ghost(int x) */;
+
+int main(){
+ return f(1, 2, 3) /*@ ghost(4) */;
+}
diff --git a/src/plugins/variadic/tests/declared/no-va.c b/src/plugins/variadic/tests/declared/no-va.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/no-va.c
rename to src/plugins/variadic/tests/declared/no-va.i
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..77d342b3dd8113ce3c181cca5993138243e6bbe4
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -0,0 +1,35 @@
+[variadic] tests/declared/empty-vpar-with-ghost.i:1:
+ Declaration of variadic function f.
+[variadic] tests/declared/empty-vpar-with-ghost.i:8:
+ Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel] tests/declared/empty-vpar-with-ghost.i:8: Warning:
+ No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+/* Generated by Frama-C */
+/*@ assigns \nothing;
+
+ behavior bhv:
+ requires c > 0;
+ requires a ≤ 42; */
+void f(int const a, int, int c, void * const *__va_params)
+ /*@ ghost (int x) */;
+
+int main(void)
+{
+ int __retres;
+ {
+ void *__va_args[1] = {(void *)0};
+ f(1,2,3,(void * const *)(__va_args)) /*@ ghost (4) */;
+ }
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
index 0603bbc1ab9646011fbd050407523a1a8fddf452..c028e9e151d91ac8f3d848668a9ead0863bef9f1 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/empty-vpar.c:1: Declaration of variadic function f.
-[variadic] tests/declared/empty-vpar.c:8:
+[variadic] tests/declared/empty-vpar.i:1: Declaration of variadic function f.
+[variadic] tests/declared/empty-vpar.i:8:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] tests/declared/empty-vpar.c:8: Warning:
+[kernel] tests/declared/empty-vpar.i:8: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f81ac2a39cfd228c91a75b2f1f0ea81f0c32a683
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
@@ -0,0 +1,42 @@
+[variadic] tests/declared/function-ptr-with-ghost.i:4:
+ Declaration of variadic function va_f.
+[variadic] tests/declared/function-ptr-with-ghost.i:2:
+ Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/function-ptr-with-ghost.i:2: Warning:
+ Neither code nor specification for function va_f, generating default assigns from the prototype
+[eva] using specification for function va_f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function function:
+
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+/* Generated by Frama-C */
+void function(void (*p)(int , void * const *__va_params) /*@ ghost (int v) */,
+ int x)
+{
+ {
+ int __va_arg0 = 1;
+ int __va_arg1 = 2;
+ int __va_arg2 = 3;
+ void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
+ (*p)(x,(void * const *)(__va_args)) /*@ ghost (4) */;
+ }
+ return;
+}
+
+/*@ assigns \nothing; */
+void va_f(int, void * const *__va_params) /*@ ghost (int x) */;
+
+int main(void)
+{
+ int __retres;
+ function(& va_f,3);
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/label.res.oracle b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
index 0c51782917566ef261529445f19a27d6fa5749b2..427868a9c76ae47b935ff087454c0ef2b589dc3d 100644
--- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/label.c:4: Declaration of variadic function f.
-[variadic] tests/declared/label.c:8:
+[variadic] tests/declared/label.i:4: Declaration of variadic function f.
+[variadic] tests/declared/label.i:8:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/label.c:8: Warning:
+[kernel:annot:missing-spec] tests/declared/label.i:8: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index 58b1c09b3834a3614654b7116de3ec709e16417d..adcbb2b04d43ce39487600c92e43c8f4c6d65a55 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -1,16 +1,16 @@
-[variadic] tests/declared/multi.c:1: Declaration of variadic function f.
-[variadic] tests/declared/multi.c:12: Declaration of variadic function g.
-[variadic] tests/declared/multi.c:9:
+[variadic] tests/declared/multi.i:1: Declaration of variadic function f.
+[variadic] tests/declared/multi.i:12: Declaration of variadic function g.
+[variadic] tests/declared/multi.i:9:
Generic translation of call to variadic function.
-[variadic] tests/declared/multi.c:18:
+[variadic] tests/declared/multi.i:18:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] tests/declared/multi.c:18: Warning:
+[kernel] tests/declared/multi.i:18: Warning:
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[eva] using specification for function g
-[kernel] tests/declared/multi.c:9: Warning:
+[kernel] tests/declared/multi.i:9: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..71fffe6ce3458de80a11bed3ab9404ef530b1137
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
@@ -0,0 +1,23 @@
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/no-va-with-ghost.i:4: Warning:
+ Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+
+/* Generated by Frama-C */
+/*@ assigns \result;
+ assigns \result \from a, b, c; */
+int f(int a, int b, int c) /*@ ghost (int x) */;
+
+int main(void)
+{
+ int tmp;
+ tmp = f(1,2,3) /*@ ghost (4) */;
+ return tmp;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
index df93a80eca42e87351c30aa535b2914f7cd8cd48..f00b72688a6be12492c6b91ac8db6c8ab0a43dcc 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
@@ -1,7 +1,7 @@
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/no-va.c:4: Warning:
+[kernel:annot:missing-spec] tests/declared/no-va.i:4: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9dde9d6d2dfbaa061b976f6f32aa14042c6fa493
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
@@ -0,0 +1,38 @@
+[variadic] tests/declared/rvalues-with-ghost.i:1:
+ Declaration of variadic function f.
+[variadic] tests/declared/rvalues-with-ghost.i:5:
+ Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/rvalues-with-ghost.i:5: Warning:
+ Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ x ∈ {0}
+ i ∈ [--..--]
+ __va_arg0 ∈ {5}
+ __va_arg1 ∈ {20}
+ __va_arg2 ∈ {{ &x }}
+ __va_args[0] ∈ {{ (void *)&__va_arg0 }}
+ [1] ∈ {{ (void *)&__va_arg1 }}
+ [2] ∈ {{ (void *)&__va_arg2 }}
+/* Generated by Frama-C */
+/*@ assigns \result;
+ assigns \result \from a; */
+int f(int a, void * const *__va_params) /*@ ghost (int x) */;
+
+int main(void)
+{
+ int x = 0;
+ int __va_arg0 = 2 + 3;
+ int __va_arg1 = 4 * 5;
+ int *__va_arg2 = & x;
+ void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
+ int i = f(1,(void * const *)(__va_args)) /*@ ghost (x + 3) */;
+ return i;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
index 99e27480afacce5296c6d5d0e4b2c5c5f387200f..82863e34c748ad7430e51e9490d9e1cdefa51f28 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/rvalues.c:1: Declaration of variadic function f.
-[variadic] tests/declared/rvalues.c:5:
+[variadic] tests/declared/rvalues.i:1: Declaration of variadic function f.
+[variadic] tests/declared/rvalues.i:5:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/rvalues.c:5: Warning:
+[kernel:annot:missing-spec] tests/declared/rvalues.i:5: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..fa2e63b8a114173eac0d131f2fe7c203d8ef6592
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -0,0 +1,40 @@
+[variadic] tests/declared/simple-with-ghost.i:1:
+ Declaration of variadic function f.
+[variadic] tests/declared/simple-with-ghost.i:9:
+ Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel] tests/declared/simple-with-ghost.i:9: Warning:
+ No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+
+/* Generated by Frama-C */
+/*@ assigns \result;
+ assigns \result \from a, c;
+
+ behavior bhv:
+ requires c > 0;
+ requires a ≤ 42;
+ ensures \result > 0;
+ */
+int f(int const a, int, int c, void * const *__va_params)
+ /*@ ghost (int x) */;
+
+int main(void)
+{
+ int tmp;
+ {
+ int __va_arg0 = 4;
+ int __va_arg1 = 5;
+ int __va_arg2 = 6;
+ void *__va_args[3] = {& __va_arg0, & __va_arg1, & __va_arg2};
+ tmp = f(1,2,3,(void * const *)(__va_args)) /*@ ghost (7) */;
+ }
+ return tmp;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
index d36878734cf263a85f28807227f051986d50fac3..9112e9470077a769eaa504faed32bb9cf3caf757 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/simple.c:1: Declaration of variadic function f.
-[variadic] tests/declared/simple.c:9:
+[variadic] tests/declared/simple.i:1: Declaration of variadic function f.
+[variadic] tests/declared/simple.i:9:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel] tests/declared/simple.c:9: Warning:
+[kernel] tests/declared/simple.i:9: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
index 37d0817d12f1fd03bf5342a582c78716c10e7749..851c21816f4c535bc3c0e443d014611b540c9768 100644
--- a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/declared/struct.c:5: Declaration of variadic function f.
-[variadic] tests/declared/struct.c:10:
+[variadic] tests/declared/struct.i:5: Declaration of variadic function f.
+[variadic] tests/declared/struct.i:10:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/struct.c:10: Warning:
+[kernel:annot:missing-spec] tests/declared/struct.i:10: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3038502c8ded9a4b0149591a360b55e8c7118292
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
@@ -0,0 +1,33 @@
+[variadic] tests/declared/typedefed_function-with-ghost.i:2:
+ Declaration of variadic function f.
+[variadic] tests/declared/typedefed_function-with-ghost.i:5:
+ Generic translation of call to variadic function.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[kernel:annot:missing-spec] tests/declared/typedefed_function-with-ghost.i:5: Warning:
+ Neither code nor specification for function f, generating default assigns from the prototype
+[eva] using specification for function f
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __retres ∈ {0}
+/* Generated by Frama-C */
+typedef void T(int , void * const *__va_params) /*@ ghost (int ) */;
+/*@ assigns \nothing; */
+extern T f;
+
+int main(void)
+{
+ int __retres;
+ {
+ int __va_arg0 = 2;
+ int __va_arg1 = 0;
+ void *__va_args[2] = {& __va_arg0, & __va_arg1};
+ f(1,(void * const *)(__va_args)) /*@ ghost (3) */;
+ }
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
index b497ee3c477f455d1f22aad98c26929e4a251716..fa5cdfe98bbd3fb99d79eaceab46e2b687038d64 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
@@ -1,11 +1,11 @@
-[variadic] tests/declared/typedefed_function.c:2:
+[variadic] tests/declared/typedefed_function.i:2:
Declaration of variadic function f.
-[variadic] tests/declared/typedefed_function.c:5:
+[variadic] tests/declared/typedefed_function.i:5:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[kernel:annot:missing-spec] tests/declared/typedefed_function.c:5: Warning:
+[kernel:annot:missing-spec] tests/declared/typedefed_function.i:5: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/declared/rvalues-with-ghost.i b/src/plugins/variadic/tests/declared/rvalues-with-ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..6452e6529824d5ff7aade70f2574f6f7c9ac4efe
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/rvalues-with-ghost.i
@@ -0,0 +1,7 @@
+int f(int a,...) /*@ ghost(int x) */;
+
+int main(){
+ int x = 0;
+ int i = f(1, 2+3, 4*5, &x) /*@ ghost(x+3) */;
+ return i;
+}
diff --git a/src/plugins/variadic/tests/declared/rvalues.c b/src/plugins/variadic/tests/declared/rvalues.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/rvalues.c
rename to src/plugins/variadic/tests/declared/rvalues.i
diff --git a/src/plugins/variadic/tests/declared/simple-with-ghost.i b/src/plugins/variadic/tests/declared/simple-with-ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..06afdffe232d2490e1e97d85dd70832a95fe9881
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/simple-with-ghost.i
@@ -0,0 +1,10 @@
+/*@ behavior bhv:
+ @ requires c>0;
+ @ requires a<=42;
+ @ ensures \result > 0;
+*/
+int f(const int a, int, int c,...) /*@ ghost (int x) */;
+
+int main(){
+ return f(1, 2, 3, 4, 5, 6) /*@ ghost(7) */;
+}
diff --git a/src/plugins/variadic/tests/declared/simple.c b/src/plugins/variadic/tests/declared/simple.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/simple.c
rename to src/plugins/variadic/tests/declared/simple.i
diff --git a/src/plugins/variadic/tests/declared/struct.c b/src/plugins/variadic/tests/declared/struct.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/struct.c
rename to src/plugins/variadic/tests/declared/struct.i
diff --git a/src/plugins/variadic/tests/declared/typedefed_function-with-ghost.i b/src/plugins/variadic/tests/declared/typedefed_function-with-ghost.i
new file mode 100644
index 0000000000000000000000000000000000000000..32116ed21ed39bb2b8ba8e1dcfed1ce3236d6770
--- /dev/null
+++ b/src/plugins/variadic/tests/declared/typedefed_function-with-ghost.i
@@ -0,0 +1,7 @@
+typedef void T(int, ...) /*@ ghost (int) */ ;
+extern T f;
+
+int main () {
+ f(1, 2, 0) /*@ ghost(3) */;
+ return 0;
+}
diff --git a/src/plugins/variadic/tests/declared/typedefed_function.c b/src/plugins/variadic/tests/declared/typedefed_function.i
similarity index 100%
rename from src/plugins/variadic/tests/declared/typedefed_function.c
rename to src/plugins/variadic/tests/declared/typedefed_function.i
diff --git a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
index 90e4c436eef05876c5fa6f7a399d1ed24a7a8cc9..9fcbfae2ed2afb6f4498cd8fc01efebb747ea53f 100644
--- a/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/recursive.res.oracle
@@ -1,14 +1,14 @@
-[variadic] tests/defined/recursive.c:4: Declaration of variadic function f.
-[variadic] tests/defined/recursive.c:8:
+[variadic] tests/defined/recursive.i:4: Declaration of variadic function f.
+[variadic] tests/defined/recursive.i:8:
Generic translation of call to variadic function.
-[variadic] tests/defined/recursive.c:12:
+[variadic] tests/defined/recursive.i:12:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] tests/defined/recursive.c:8: Warning:
+[eva] tests/defined/recursive.i:8: Warning:
recursive call during value analysis
- of f (f <- f :: tests/defined/recursive.c:12 <- main). Assuming the call has
+ of f (f <- f :: tests/defined/recursive.i:12 <- main). Assuming the call has
no effect. The analysis will be unsound.
[eva] using specification for function f
[eva] done for function main
diff --git a/src/plugins/variadic/tests/defined/recursive.c b/src/plugins/variadic/tests/defined/recursive.i
similarity index 100%
rename from src/plugins/variadic/tests/defined/recursive.c
rename to src/plugins/variadic/tests/defined/recursive.i
diff --git a/src/plugins/variadic/tests/erroneous/invalid_libc.c b/src/plugins/variadic/tests/erroneous/invalid_libc.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/invalid_libc.c
rename to src/plugins/variadic/tests/erroneous/invalid_libc.i
diff --git a/src/plugins/variadic/tests/erroneous/no-libc.c b/src/plugins/variadic/tests/erroneous/no-libc.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/no-libc.c
rename to src/plugins/variadic/tests/erroneous/no-libc.i
diff --git a/src/plugins/variadic/tests/erroneous/no-param.c b/src/plugins/variadic/tests/erroneous/no-param.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/no-param.c
rename to src/plugins/variadic/tests/erroneous/no-param.i
diff --git a/src/plugins/variadic/tests/erroneous/not-enough-par.c b/src/plugins/variadic/tests/erroneous/not-enough-par.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/not-enough-par.c
rename to src/plugins/variadic/tests/erroneous/not-enough-par.i
diff --git a/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle
index de3bfcfe76b1ff09db17d7ec9e9bc67d88a32627..321767e52205d5455405b950258b4c4928dab8cd 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/invalid_libc.res.oracle
@@ -1,7 +1,7 @@
-[variadic] tests/erroneous/invalid_libc.c:2:
+[variadic] tests/erroneous/invalid_libc.i:2:
Declaration of variadic function fprintf.
-[variadic] tests/erroneous/invalid_libc.c:2: Warning:
+[variadic] tests/erroneous/invalid_libc.i:2: Warning:
The standard function fprintf was expected to have at least 2 fixed parameters but only has 1.
No variadic translation will be performed.
-[variadic] tests/erroneous/invalid_libc.c:6:
+[variadic] tests/erroneous/invalid_libc.i:6:
Generic translation of call to variadic function.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle
index 121d95f029cf9c1cb126173e22f4dee7ec656c8a..64101cd01a75097315b353cb57906d47cfb2b087 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/no-libc.res.oracle
@@ -1,5 +1,5 @@
-[variadic] tests/erroneous/no-libc.c:1: Declaration of variadic function printf.
+[variadic] tests/erroneous/no-libc.i:1: Declaration of variadic function printf.
[variadic] Warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
[variadic] Warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
-[variadic] tests/erroneous/no-libc.c:5:
+[variadic] tests/erroneous/no-libc.i:5:
Translating call to printf to a call to the specialized version printf_va_1.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
index 82b7439890793d48dc358156d48bcee6e153366e..c05a4ba9b29af3af3f01dcbf46d240984404e5b4 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/not-enough-par.res.oracle
@@ -1,5 +1,4 @@
-[kernel] tests/erroneous/not-enough-par.c:4: User Error:
+[kernel] tests/erroneous/not-enough-par.i:4: User Error:
Too few arguments in call to f.
-[kernel] User Error: stopping on file "tests/erroneous/not-enough-par.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
+[kernel] User Error: stopping on file "tests/erroneous/not-enough-par.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
index 780e418ed94a3b3f92cfd3721e4789ae5b6c793f..30f7e2cf18c5d3543616fe729f4c0856b7693785 100644
--- a/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
+++ b/src/plugins/variadic/tests/erroneous/oracle/variadic-builtin.res.oracle
@@ -1,4 +1,4 @@
-[variadic] tests/erroneous/variadic-builtin.c:1:
+[variadic] tests/erroneous/variadic-builtin.i:1:
Variadic builtin Frama_C_show_each_warning left untransformed.
[kernel] Plug-in variadic aborted: unimplemented feature.
You may send a feature request at http://bts.frama-c.com with:
diff --git a/src/plugins/variadic/tests/erroneous/variadic-builtin.c b/src/plugins/variadic/tests/erroneous/variadic-builtin.i
similarity index 100%
rename from src/plugins/variadic/tests/erroneous/variadic-builtin.c
rename to src/plugins/variadic/tests/erroneous/variadic-builtin.i
diff --git a/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
index 9b7494fd8342d16b8e56adb562b395d9c87edb25..41b4f0c4fb811f31682c40d4a3d82aba5efd6ef7 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_redefined.res.oracle
@@ -1,10 +1,10 @@
-[variadic] tests/known/printf_redefined.c:3:
+[variadic] tests/known/printf_redefined.i:3:
Declaration of variadic function printf.
[variadic] Warning: Unable to locate ACSL predicate valid_read_string which should be in the Frama-C LibC. Correct specifications can't be generated.
[variadic] Warning: Unable to locate global __fc_stdout which should be in the Frama-C LibC. Correct specifications can't be generated.
-[variadic] tests/known/printf_redefined.c:7:
+[variadic] tests/known/printf_redefined.i:7:
Translating call to printf to a call to the specialized version printf_va_1.
-[variadic] tests/known/printf_redefined.c:7: Warning:
+[variadic] tests/known/printf_redefined.i:7: Warning:
Incorrect type for argument 2. The argument will be cast from long to size_t.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
diff --git a/src/plugins/variadic/tests/known/printf_redefined.c b/src/plugins/variadic/tests/known/printf_redefined.i
similarity index 100%
rename from src/plugins/variadic/tests/known/printf_redefined.c
rename to src/plugins/variadic/tests/known/printf_redefined.i
diff --git a/src/plugins/variadic/translate.ml b/src/plugins/variadic/translate.ml
index 0dbf07862c4da167cad784fc1e547b6b06f098f9..6e7e7c7212514305affbbdb957b0f0facbb6de33 100644
--- a/src/plugins/variadic/translate.ml
+++ b/src/plugins/variadic/translate.ml
@@ -173,7 +173,8 @@ let translate_variadics (file : file) =
| Call(lv, callee, args, loc) ->
let is_variadic =
try
- let last = Extends.List.last (Typ.params (Cil.typeOf callee)) in
+ let args, _ = Typ.ghost_partitioned_params (Cil.typeOf callee) in
+ let last = Extends.List.last args in
last = Generic.vpar
with Extends.List.EmptyList -> false
in
diff --git a/tests/misc/Change_formals.ml b/tests/cil/Change_formals.ml
similarity index 100%
rename from tests/misc/Change_formals.ml
rename to tests/cil/Change_formals.ml
diff --git a/tests/cil/change_formals.c b/tests/cil/change_formals.c
new file mode 100644
index 0000000000000000000000000000000000000000..5ac6f89b75edfa8287197e7faefe404870c75820
--- /dev/null
+++ b/tests/cil/change_formals.c
@@ -0,0 +1,17 @@
+/* run.config
+EXECNOW: make -s tests/cil/Change_formals.cmxs
+OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print
+OPT: -load-module tests/cil/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print
+OPT: -load-module tests/cil/Change_formals.cmxs -then-on test -print
+*/
+
+#ifndef NO_PROTO
+int f(int x);
+#endif
+
+#ifndef NO_IMPLEM
+int f(int x) { return x; }
+#endif
+
+// needed to prevent erasure of f in NO_IMPLEM case
+int g() { return f(0); }
diff --git a/tests/cil/insert_formal.i b/tests/cil/insert_formal.i
new file mode 100644
index 0000000000000000000000000000000000000000..d6222ef953c9ff024b70b15790c0599661a69875
--- /dev/null
+++ b/tests/cil/insert_formal.i
@@ -0,0 +1,104 @@
+/* run.config
+MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+OPT: -print
+*/
+
+// v
+void void_circumflex( void ) {
+
+}
+
+// v
+void void_circumflex_g( void ) {
+
+}
+
+// v
+void void_dollar( void ) {
+
+}
+
+// v
+void void_dollar_g( void ) {
+
+}
+
+// v
+void a_circumflex( int a ) {
+
+}
+
+// v
+void a_dollar( int a ) {
+
+}
+
+// v
+void a_circumflex_g( int a ) {
+
+}
+
+// v
+void a_dollar_g( int a ) {
+
+}
+
+// v
+void a_a( int a ){
+
+}
+
+// v
+void ghost_a_circumflex( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_dollar( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_circumflex_g( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_dollar_g( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void ghost_a_a( void ) /*@ ghost ( int a ) */ {
+
+}
+
+// v
+void a_b_c_a (int a, int b, int c) {
+
+}
+
+// v
+void b_a_c_a (int b, int a, int c) {
+
+}
+
+// v
+void all_ghost_a_b_c_a ( void )/*@ ghost (int a, int b, int c) */ {
+
+}
+
+// v
+void all_ghost_b_a_c_a ( void )/*@ ghost (int b, int a, int c) */ {
+
+}
+
+// v
+void a_ghost_b_c_a ( int a )/*@ ghost (int b, int c) */ {
+
+}
+
+// v
+void b_ghost_a_c_a ( int b )/*@ ghost (int a, int c) */ {
+
+}
diff --git a/tests/cil/insert_formal.ml b/tests/cil/insert_formal.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0a0a7e013955303b51259055161c3e30a9526836
--- /dev/null
+++ b/tests/cil/insert_formal.ml
@@ -0,0 +1,53 @@
+open Cil_types
+
+let update_func f =
+ let insert_circ f = Cil.makeFormalVar f ~where:"^" "x" Cil.intType in
+ let insert_dollar f = Cil.makeFormalVar f ~where:"$" "x" Cil.intType in
+ let insert_circ_g f = Cil.makeFormalVar f ~ghost:true ~where:"^" "x" Cil.intType in
+ let insert_dollar_g f = Cil.makeFormalVar f ~ghost:true ~where:"$" "x" Cil.intType in
+ let insert_a f = Cil.makeFormalVar f ~where:"a" "x" Cil.intType in
+ let insert_a_g f = Cil.makeFormalVar f ~ghost:true ~where:"a" "x" Cil.intType in
+ let circ_list = [
+ "void_circumflex" ;
+ "a_circumflex" ;
+ "ghost_a_circumflex"
+ ] in
+ let dollar_list = [
+ "void_dollar" ;
+ "a_dollar" ;
+ "ghost_a_dollar"
+ ] in
+ let circ_g_list = [
+ "void_circumflex_g" ;
+ "a_circumflex_g" ;
+ "ghost_a_circumflex_g"
+ ] in
+ let dollar_g_list = [
+ "void_dollar_g" ;
+ "a_dollar_g" ;
+ "ghost_a_dollar_g"
+ ] in
+ let a_list = [
+ "a_a" ;
+ "a_b_c_a" ;
+ "b_a_c_a" ;
+ "a_ghost_b_c_a" ;
+ ] in
+ let a_g_list = [
+ "ghost_a_a" ;
+ "all_ghost_a_b_c_a" ;
+ "all_ghost_b_a_c_a" ;
+ "b_ghost_a_c_a"
+ ] in
+ if List.mem f.svar.vname circ_list then ignore(insert_circ f) ;
+ if List.mem f.svar.vname dollar_list then ignore(insert_dollar f) ;
+ if List.mem f.svar.vname circ_g_list then ignore(insert_circ_g f) ;
+ if List.mem f.svar.vname dollar_g_list then ignore(insert_dollar_g f) ;
+ if List.mem f.svar.vname a_list then ignore(insert_a f) ;
+ if List.mem f.svar.vname a_g_list then ignore(insert_a_g f) ;
+ ()
+
+let run () =
+ Globals.Functions.iter_on_fundecs update_func
+
+let () = Db.Main.extend run
diff --git a/tests/misc/oracle/change_formals.0.res.oracle b/tests/cil/oracle/change_formals.0.res.oracle
similarity index 75%
rename from tests/misc/oracle/change_formals.0.res.oracle
rename to tests/cil/oracle/change_formals.0.res.oracle
index 22dc10f37e8a0e84a256544ee404ff1e529bcd10..794634cc91e1d6d84d9f983b9b9a68b9e869e1d5 100644
--- a/tests/misc/oracle/change_formals.0.res.oracle
+++ b/tests/cil/oracle/change_formals.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
[test] current prj = project "test"
[test] current prj = project "test"
/* Generated by Frama-C */
diff --git a/tests/misc/oracle/change_formals.1.res.oracle b/tests/cil/oracle/change_formals.1.res.oracle
similarity index 69%
rename from tests/misc/oracle/change_formals.1.res.oracle
rename to tests/cil/oracle/change_formals.1.res.oracle
index 1f5fcdcd5e9190f8f8d30d8539dc1445a9034ed0..0269f038c67b179ed56aa983d0535dd43b6a6fc4 100644
--- a/tests/misc/oracle/change_formals.1.res.oracle
+++ b/tests/cil/oracle/change_formals.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
[test] current prj = project "test"
/* Generated by Frama-C */
int f(int x, int ok);
diff --git a/tests/misc/oracle/change_formals.2.res.oracle b/tests/cil/oracle/change_formals.2.res.oracle
similarity index 77%
rename from tests/misc/oracle/change_formals.2.res.oracle
rename to tests/cil/oracle/change_formals.2.res.oracle
index 3f746d6b7f699a77b6f8d4fff112a9d72aa9ea18..9e91be519b33bd2915fe44dc2286eb5c28d291bc 100644
--- a/tests/misc/oracle/change_formals.2.res.oracle
+++ b/tests/cil/oracle/change_formals.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/misc/change_formals.c (with preprocessing)
+[kernel] Parsing tests/cil/change_formals.c (with preprocessing)
[test] current prj = project "test"
[test] current prj = project "test"
/* Generated by Frama-C */
diff --git a/tests/cil/oracle/insert_formal.res.oracle b/tests/cil/oracle/insert_formal.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..faefb89b04774d031958731f2df0f3da1dc8176c
--- /dev/null
+++ b/tests/cil/oracle/insert_formal.res.oracle
@@ -0,0 +1,103 @@
+[kernel] Parsing tests/cil/insert_formal.i (no preprocessing)
+/* Generated by Frama-C */
+void void_circumflex(int x)
+{
+ return;
+}
+
+void void_circumflex_g(void) /*@ ghost (int x) */
+{
+ return;
+}
+
+void void_dollar(int x)
+{
+ return;
+}
+
+void void_dollar_g(void) /*@ ghost (int x) */
+{
+ return;
+}
+
+void a_circumflex(int x, int a)
+{
+ return;
+}
+
+void a_dollar(int a, int x)
+{
+ return;
+}
+
+void a_circumflex_g(int a) /*@ ghost (int x) */
+{
+ return;
+}
+
+void a_dollar_g(int a) /*@ ghost (int x) */
+{
+ return;
+}
+
+void a_a(int a, int x)
+{
+ return;
+}
+
+void ghost_a_circumflex(int x) /*@ ghost (int a) */
+{
+ return;
+}
+
+void ghost_a_dollar(int x) /*@ ghost (int a) */
+{
+ return;
+}
+
+void ghost_a_circumflex_g(void) /*@ ghost (int x, int a) */
+{
+ return;
+}
+
+void ghost_a_dollar_g(void) /*@ ghost (int a, int x) */
+{
+ return;
+}
+
+void ghost_a_a(void) /*@ ghost (int a, int x) */
+{
+ return;
+}
+
+void a_b_c_a(int a, int x, int b, int c)
+{
+ return;
+}
+
+void b_a_c_a(int b, int a, int x, int c)
+{
+ return;
+}
+
+void all_ghost_a_b_c_a(void) /*@ ghost (int a, int x, int b, int c) */
+{
+ return;
+}
+
+void all_ghost_b_a_c_a(void) /*@ ghost (int b, int a, int x, int c) */
+{
+ return;
+}
+
+void a_ghost_b_c_a(int a, int x) /*@ ghost (int b, int c) */
+{
+ return;
+}
+
+void b_ghost_a_c_a(int b) /*@ ghost (int a, int x, int c) */
+{
+ return;
+}
+
+
diff --git a/tests/misc/change_formals.c b/tests/misc/change_formals.c
deleted file mode 100644
index c84ec7afadef6caf0fe82ca4d74cb4c1521062a2..0000000000000000000000000000000000000000
--- a/tests/misc/change_formals.c
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config
-EXECNOW: make -s tests/misc/Change_formals.cmxs
-OPT: -load-module tests/misc/Change_formals.cmxs -cpp-extra-args="-DNO_PROTO" -then-on test -print
-OPT: -load-module tests/misc/Change_formals.cmxs -cpp-extra-args="-DNO_IMPLEM" -then-on test -print
-OPT: -load-module tests/misc/Change_formals.cmxs -then-on test -print
-*/
-
-#ifndef NO_PROTO
-int f(int x);
-#endif
-
-#ifndef NO_IMPLEM
-int f(int x) { return x; }
-#endif
-
-// needed to prevent erasure of f in NO_IMPLEM case
-int g() { return f(0); }
diff --git a/tests/pretty_printing/ghost_parameters.c b/tests/pretty_printing/ghost_parameters.c
new file mode 100644
index 0000000000000000000000000000000000000000..b6faaf2100018a347a525b9d92c1f1204765c9b6
--- /dev/null
+++ b/tests/pretty_printing/ghost_parameters.c
@@ -0,0 +1,47 @@
+void decl_function_void_no_ghost(void);
+void def_function_void_no_ghost(void) {}
+void decl_function_void_ghost(void) /*@ ghost (int y) */;
+void def_function_void_ghost(void) /*@ ghost (int y) */ {}
+void decl_function_x_no_ghost(int x);
+void def_function_x_no_ghost(int x) {}
+void decl_function_x_ghost(int x) /*@ ghost (int y) */;
+void def_function_x_ghost(int x) /*@ ghost (int y) */ {}
+void decl_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */);
+void def_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */) {
+ void (*local)(int) /*@ ghost (int) */ = ptr;
+
+ (*local)(4) /*@ ghost(2) */;
+ //@ ghost (*local) (4, 2) ;
+}
+void decl_variadic(int x, ...) /*@ ghost(int y) */;
+void def_variadic(int x, ...) /*@ ghost(int y) */ {}
+
+int main(void) {
+ decl_function_void_no_ghost();
+ def_function_void_no_ghost();
+ decl_function_void_ghost() /*@ ghost (4) */;
+ def_function_void_ghost() /*@ ghost (4) */;
+ decl_function_x_no_ghost(2);
+ def_function_x_no_ghost(2);
+ decl_function_x_ghost(2) /*@ ghost (4) */;
+ def_function_x_ghost(2) /*@ ghost (4) */;
+ decl_with_fptr(&decl_function_x_ghost);
+ def_with_fptr(&decl_function_x_ghost);
+ decl_variadic(2, 1, 2, 3, 4) /*@ ghost(4) */;
+ def_variadic(2, 1, 2, 3, 4) /*@ ghost(4) */;
+
+ /*@ ghost
+ decl_function_void_no_ghost();
+ def_function_void_no_ghost();
+ decl_function_void_ghost(4);
+ def_function_void_ghost(4);
+ decl_function_x_no_ghost(2);
+ def_function_x_no_ghost(2);
+ decl_function_x_ghost(2,4);
+ def_function_x_ghost(2,4);
+ decl_with_fptr(&decl_function_x_ghost);
+ def_with_fptr(&decl_function_x_ghost);
+ decl_variadic(2, 1, 2, 3, 4, 4);
+ def_variadic(2, 1, 2, 3, 4, 4);
+ */
+}
\ No newline at end of file
diff --git a/tests/pretty_printing/oracle/ghost_parameters.res.oracle b/tests/pretty_printing/oracle/ghost_parameters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..79cdc64d68cd8d06e45db07a2084eac9205b38b4
--- /dev/null
+++ b/tests/pretty_printing/oracle/ghost_parameters.res.oracle
@@ -0,0 +1,173 @@
+[kernel] Parsing tests/pretty_printing/ghost_parameters.c (with preprocessing)
+/* Generated by Frama-C */
+void decl_function_void_no_ghost(void);
+
+void def_function_void_no_ghost(void)
+{
+ return;
+}
+
+void decl_function_void_ghost(void) /*@ ghost (int y) */;
+
+void def_function_void_ghost(void) /*@ ghost (int y) */
+{
+ return;
+}
+
+void decl_function_x_no_ghost(int x);
+
+void def_function_x_no_ghost(int x)
+{
+ return;
+}
+
+void decl_function_x_ghost(int x) /*@ ghost (int y) */;
+
+void def_function_x_ghost(int x) /*@ ghost (int y) */
+{
+ return;
+}
+
+void decl_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */);
+
+void def_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */)
+{
+ void (*local)(int ) /*@ ghost (int ) */ = ptr;
+ (*local)(4) /*@ ghost (2) */;
+ /*@ ghost (*local)(4,2); */
+ return;
+}
+
+void decl_variadic(int x , ...) /*@ ghost (int y) */;
+
+void def_variadic(int x , ...) /*@ ghost (int y) */
+{
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ decl_function_void_no_ghost();
+ def_function_void_no_ghost();
+ decl_function_void_ghost() /*@ ghost (4) */;
+ def_function_void_ghost() /*@ ghost (4) */;
+ decl_function_x_no_ghost(2);
+ def_function_x_no_ghost(2);
+ decl_function_x_ghost(2) /*@ ghost (4) */;
+ def_function_x_ghost(2) /*@ ghost (4) */;
+ decl_with_fptr(& decl_function_x_ghost);
+ def_with_fptr(& decl_function_x_ghost);
+ decl_variadic(2,1,2,3,4) /*@ ghost (4) */;
+ def_variadic(2,1,2,3,4) /*@ ghost (4) */;
+ /*@ ghost decl_function_void_no_ghost(); */
+ /*@ ghost def_function_void_no_ghost(); */
+ /*@ ghost decl_function_void_ghost(4); */
+ /*@ ghost def_function_void_ghost(4); */
+ /*@ ghost decl_function_x_no_ghost(2); */
+ /*@ ghost def_function_x_no_ghost(2); */
+ /*@ ghost decl_function_x_ghost(2,4); */
+ /*@ ghost def_function_x_ghost(2,4); */
+ /*@ ghost decl_with_fptr(& decl_function_x_ghost); */
+ /*@ ghost def_with_fptr(& decl_function_x_ghost); */
+ /*@ ghost decl_variadic(2,1,2,3,4,4); */
+ /*@ ghost def_variadic(2,1,2,3,4,4); */
+ __retres = 0;
+ return __retres;
+}
+
+
+[kernel] Parsing tests/pretty_printing/result/ghost_parameters.c (with preprocessing)
+[kernel] Parsing tests/pretty_printing/ghost_parameters.c (with preprocessing)
+[kernel] tests/pretty_printing/ghost_parameters.c:2: Warning:
+ dropping duplicate def'n of func def_function_void_no_ghost at tests/pretty_printing/ghost_parameters.c:2 in favor of that at tests/pretty_printing/result/ghost_parameters.c:4
+[kernel] tests/pretty_printing/ghost_parameters.c:4: Warning:
+ dropping duplicate def'n of func def_function_void_ghost at tests/pretty_printing/ghost_parameters.c:4 in favor of that at tests/pretty_printing/result/ghost_parameters.c:11
+[kernel] tests/pretty_printing/ghost_parameters.c:6: Warning:
+ dropping duplicate def'n of func def_function_x_no_ghost at tests/pretty_printing/ghost_parameters.c:6 in favor of that at tests/pretty_printing/result/ghost_parameters.c:18
+[kernel] tests/pretty_printing/ghost_parameters.c:8: Warning:
+ dropping duplicate def'n of func def_function_x_ghost at tests/pretty_printing/ghost_parameters.c:8 in favor of that at tests/pretty_printing/result/ghost_parameters.c:25
+[kernel] tests/pretty_printing/ghost_parameters.c:10: Warning:
+ dropping duplicate def'n of func def_with_fptr at tests/pretty_printing/ghost_parameters.c:10 in favor of that at tests/pretty_printing/result/ghost_parameters.c:32
+[kernel] tests/pretty_printing/ghost_parameters.c:17: Warning:
+ dropping duplicate def'n of func def_variadic at tests/pretty_printing/ghost_parameters.c:17 in favor of that at tests/pretty_printing/result/ghost_parameters.c:42
+[kernel] tests/pretty_printing/ghost_parameters.c:19: Warning:
+ def'n of func main at tests/pretty_printing/ghost_parameters.c:19 (sum 21482) conflicts with the one at tests/pretty_printing/result/ghost_parameters.c:47 (sum 23256); keeping the one at tests/pretty_printing/result/ghost_parameters.c:47.
+/* Generated by Frama-C */
+void decl_function_void_no_ghost(void);
+
+void def_function_void_no_ghost(void)
+{
+ return;
+}
+
+void decl_function_void_ghost(void) /*@ ghost (int y) */;
+
+void def_function_void_ghost(void) /*@ ghost (int y) */
+{
+ return;
+}
+
+void decl_function_x_no_ghost(int x);
+
+void def_function_x_no_ghost(int x)
+{
+ return;
+}
+
+void decl_function_x_ghost(int x) /*@ ghost (int y) */;
+
+void def_function_x_ghost(int x) /*@ ghost (int y) */
+{
+ return;
+}
+
+void decl_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */);
+
+void def_with_fptr(void (*ptr)(int x) /*@ ghost (int y) */)
+{
+ void (*local)(int ) /*@ ghost (int ) */ = ptr;
+ (*local)(4) /*@ ghost (2) */;
+ /*@ ghost (*local)(4,2); */
+ return;
+}
+
+void decl_variadic(int x , ...) /*@ ghost (int y) */;
+
+void def_variadic(int x , ...) /*@ ghost (int y) */
+{
+ return;
+}
+
+int main(void)
+{
+ int __retres;
+ decl_function_void_no_ghost();
+ def_function_void_no_ghost();
+ decl_function_void_ghost() /*@ ghost (4) */;
+ def_function_void_ghost() /*@ ghost (4) */;
+ decl_function_x_no_ghost(2);
+ def_function_x_no_ghost(2);
+ decl_function_x_ghost(2) /*@ ghost (4) */;
+ def_function_x_ghost(2) /*@ ghost (4) */;
+ decl_with_fptr(& decl_function_x_ghost);
+ def_with_fptr(& decl_function_x_ghost);
+ decl_variadic(2,1,2,3,4) /*@ ghost (4) */;
+ def_variadic(2,1,2,3,4) /*@ ghost (4) */;
+ /*@ ghost decl_function_void_no_ghost(); */
+ /*@ ghost def_function_void_no_ghost(); */
+ /*@ ghost decl_function_void_ghost(4); */
+ /*@ ghost def_function_void_ghost(4); */
+ /*@ ghost decl_function_x_no_ghost(2); */
+ /*@ ghost def_function_x_no_ghost(2); */
+ /*@ ghost decl_function_x_ghost(2,4); */
+ /*@ ghost def_function_x_ghost(2,4); */
+ /*@ ghost decl_with_fptr(& decl_function_x_ghost); */
+ /*@ ghost def_with_fptr(& decl_function_x_ghost); */
+ /*@ ghost decl_variadic(2,1,2,3,4,4); */
+ /*@ ghost def_variadic(2,1,2,3,4,4); */
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/spec/assigns_from_kf.i b/tests/spec/assigns_from_kf.i
new file mode 100644
index 0000000000000000000000000000000000000000..cf8f4228ed4bbb3f61a637e1508e6d97315ecbd9
--- /dev/null
+++ b/tests/spec/assigns_from_kf.i
@@ -0,0 +1,27 @@
+/* run.config
+ MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -print
+*/
+
+void nothing(void);
+int nothing_r(void);
+
+void something_non_ghost(int *p);
+void something_ghost(void) /*@ ghost (int* p) */;
+
+int something_non_ghost_r(int *p);
+int something_ghost_r(void) /*@ ghost (int* p) */;
+
+void both(int* p, int x) /*@ ghost (int* gp, int gx) */;
+int both_r(int* p, int x) /*@ ghost (int* gp, int gx) */;
+
+void reference(void) {
+ nothing();
+ nothing_r();
+ something_non_ghost(0);
+ something_ghost() /*@ ghost (0) */;
+ something_non_ghost_r(0);
+ something_ghost_r() /*@ ghost (0) */;
+ both(0, 1) /*@ ghost (0, 2) */;
+ both_r(0, 1) /*@ ghost (0, 2) */;
+}
\ No newline at end of file
diff --git a/tests/spec/assigns_from_kf.ml b/tests/spec/assigns_from_kf.ml
new file mode 100644
index 0000000000000000000000000000000000000000..fcab8e135d1e04408c95c695eba44eac20e22173
--- /dev/null
+++ b/tests/spec/assigns_from_kf.ml
@@ -0,0 +1,4 @@
+let run () =
+ Globals.Functions.iter (fun kf -> ignore (Annotations.funspec kf))
+
+let () = Db.Main.extend run
\ No newline at end of file
diff --git a/tests/spec/oracle/assigns_from_kf.res.oracle b/tests/spec/oracle/assigns_from_kf.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ac10b7070c2d88b55fd1b456f5a3a9ac30099cdf
--- /dev/null
+++ b/tests/spec/oracle/assigns_from_kf.res.oracle
@@ -0,0 +1,71 @@
+[kernel] Parsing tests/spec/assigns_from_kf.i (no preprocessing)
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function both, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function both_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function nothing, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function nothing_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function something_ghost, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function something_ghost_r, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function something_non_ghost, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/spec/assigns_from_kf.i:18: Warning:
+ Neither code nor specification for function something_non_ghost_r, generating default assigns from the prototype
+/* Generated by Frama-C */
+/*@ assigns \nothing; */
+void nothing(void);
+
+/*@ assigns \result;
+ assigns \result \from \nothing; */
+int nothing_r(void);
+
+/*@ assigns *p;
+ assigns *p \from *p; */
+void something_non_ghost(int *p);
+
+/*@ assigns *p;
+ assigns *p \from *p; */
+void something_ghost(void) /*@ ghost (int *p) */;
+
+/*@ assigns \result, *p;
+ assigns \result \from *p;
+ assigns *p \from *p; */
+int something_non_ghost_r(int *p);
+
+/*@ assigns \result, *p;
+ assigns \result \from \nothing;
+ assigns *p \from *p;
+ */
+int something_ghost_r(void) /*@ ghost (int *p) */;
+
+/*@ assigns *p, *gp;
+ assigns *p \from *p, x;
+ assigns *gp \from *p, *gp, x, gx;
+ */
+void both(int *p, int x) /*@ ghost (int *gp, int gx) */;
+
+/*@ assigns \result, *p, *gp;
+ assigns \result \from *p, x;
+ assigns *p \from *p, x;
+ assigns *gp \from *p, *gp, x, gx;
+ */
+int both_r(int *p, int x) /*@ ghost (int *gp, int gx) */;
+
+void reference(void)
+{
+ nothing();
+ nothing_r();
+ something_non_ghost((int *)0);
+ something_ghost() /*@ ghost ((int *)0) */;
+ something_non_ghost_r((int *)0);
+ something_ghost_r() /*@ ghost ((int *)0) */;
+ both((int *)0,1) /*@ ghost ((int *)0,2) */;
+ both_r((int *)0,1) /*@ ghost ((int *)0,2) */;
+ return;
+}
+
+
diff --git a/tests/syntax/ghost_func_ptr.i b/tests/syntax/ghost_func_ptr.i
new file mode 100644
index 0000000000000000000000000000000000000000..ba5ce7a1911a6eca9b0045ed36ef926977428985
--- /dev/null
+++ b/tests/syntax/ghost_func_ptr.i
@@ -0,0 +1,5 @@
+//@ ghost void (*g)(int *) = 0 ;
+
+int main(){
+ //@ ghost void (*l)(int *) = 0 ;
+}
diff --git a/tests/syntax/ghost_parameters.c b/tests/syntax/ghost_parameters.c
new file mode 100644
index 0000000000000000000000000000000000000000..5aae254922897843c44c6eca66dda28045391c43
--- /dev/null
+++ b/tests/syntax/ghost_parameters.c
@@ -0,0 +1,208 @@
+/* run.config
+ STDOPT: +" -cpp-extra-args=-DARGS_NOT_VOID"
+ STDOPT: +" -cpp-extra-args=-DARGS_VOID"
+ STDOPT: +" -cpp-extra-args=-DCOHERENT_DECL"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_LOCAL_DECL_NON_GHOST"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_GLOBAL_DECL_NON_GHOST"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_LOCAL_DECL_GHOST"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_GLOBAL_DECL_GHOST"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_LOCAL_DECL_MORE_GHOSTS"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_GLOBAL_DECL_MORE_GHOSTS"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_LOCAL_DECL_MORE_NON_GHOSTS"
+ STDOPT: +" -cpp-extra-args=-DINCOHERENT_GLOBAL_DECL_MORE_NON_GHOSTS"
+ STDOPT: +" -cpp-extra-args=-DVOID_EMPTY_GHOST_PARAMETER_LIST"
+ STDOPT: +" -cpp-extra-args=-DVOID_GHOST_PARAMETER"
+*/
+
+#ifdef ARGS_NOT_VOID
+
+void function(int a, int b) /*@ ghost (int c, int d) */{
+
+}
+
+void caller(void){
+ // VALID
+ function(1, 2) /*@ ghost (3, 4)*/ ;
+ /*@ ghost function(1, 2, 3, 4) ; */
+
+ // INVALID
+ function(1, 2) ;
+ function(1, 2) /*@ ghost (3) */ ;
+ function(1) /*@ ghost (2, 3) */ ;
+ function(1, 2, 3, 4) ;
+ function() /*@ ghost (1, 2, 3, 4) */ ;
+
+ /*@ ghost function(1, 2) ; */
+ /*@ ghost function(1) ; */
+ /*@ ghost function(1, 2, 3) ; */
+}
+
+#endif
+
+#ifdef ARGS_VOID
+
+void function(void) /*@ ghost (int c, int d) */{
+
+}
+
+void caller(void){
+ // VALID
+ function() /*@ ghost (3, 4)*/ ;
+ /*@ ghost function(3, 4) ; */
+
+ // INVALID
+ function() ;
+ function() /*@ ghost (3) */ ;
+ function(1) /*@ ghost (2, 3) */ ;
+ function(1, 2) ;
+ function() /*@ ghost (1, 2, 3) */ ;
+
+ /*@ ghost function() ; */
+ /*@ ghost function(1) ; */
+ /*@ ghost function(1, 2, 3) ; */
+}
+
+#endif
+
+#ifdef COHERENT_DECL
+
+void caller(void){
+ void function(int a, int b) /*@ ghost(int c, int d) */ ;
+ function(1, 2) /*@ ghost (3, 4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ ;
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_LOCAL_DECL_NON_GHOST
+
+void caller(void){
+ void function(int b) /*@ ghost(int c, int d) */ ;
+ function(2) /*@ ghost (3, 4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_GLOBAL_DECL_NON_GHOST
+
+void function(int b) /*@ ghost(int c, int d) */ ;
+
+void caller(void){
+ function(2) /*@ ghost (3, 4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_LOCAL_DECL_GHOST
+
+void caller(void){
+ void function(int a, int b) /*@ ghost(int d) */ ;
+ function(1, 2) /*@ ghost (4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_GLOBAL_DECL_GHOST
+
+void function(int a, int b) /*@ ghost(int d) */ ;
+
+void caller(void){
+ function(1, 2) /*@ ghost (3) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_LOCAL_DECL_MORE_GHOSTS
+
+void caller(void){
+ void function(int a, int b, int c) /*@ ghost(int d) */ ;
+ function(1, 2, 3) /*@ ghost (4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_GLOBAL_DECL_MORE_GHOSTS
+
+void function(int a, int b, int c) /*@ ghost(int d) */ ;
+
+void caller(void){
+ function(1, 2, 3) /*@ ghost (4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_LOCAL_DECL_MORE_NON_GHOSTS
+
+void caller(void){
+ void function(int a) /*@ ghost(int b, int c, int d) */ ;
+ function(1) /*@ ghost (2, 3, 4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef INCOHERENT_GLOBAL_DECL_MORE_NON_GHOSTS
+
+void function(int a) /*@ ghost(int b, int c, int d) */ ;
+
+void caller(void){
+ function(1) /*@ ghost (2, 3, 4) */ ;
+}
+
+void function(int a, int b) /*@ ghost(int c, int d) */ {
+
+}
+
+#endif
+
+#ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
+
+void function_void(void) /*@ ghost () */ {
+
+}
+
+#endif
+
+#ifdef VOID_GHOST_PARAMETER
+
+void function_void(void) /*@ ghost (void) */ {
+
+}
+
+void function_non_void(int x) /*@ ghost (void) */ {
+
+}
+
+#endif
\ No newline at end of file
diff --git a/tests/syntax/ghost_parameters_formals_status.i b/tests/syntax/ghost_parameters_formals_status.i
new file mode 100644
index 0000000000000000000000000000000000000000..4698b9f77e2e313d832db47fc4a41b83371508e5
--- /dev/null
+++ b/tests/syntax/ghost_parameters_formals_status.i
@@ -0,0 +1,22 @@
+/* run.config
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ OPT: -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
+*/
+
+void declaration_void(void) /*@ ghost (int x, int y) */ ;
+void declaration_not_void(int a, int b) /*@ ghost (int x, int y) */ ;
+
+void definition_void(void) /*@ ghost(int x, int y) */ {
+
+}
+
+void definition_not_void(int a, int b) /*@ ghost(int x, int y) */ {
+
+}
+
+void caller(){
+ declaration_void() /*@ ghost (1, 2) */ ;
+ declaration_not_void(1, 2) /*@ ghost (3, 4) */ ;
+ definition_void() /*@ ghost (1, 2) */ ;
+ definition_not_void(1, 2) /*@ ghost (3, 4) */ ;
+}
diff --git a/tests/syntax/ghost_parameters_formals_status.ml b/tests/syntax/ghost_parameters_formals_status.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9181658f40760e61e3572a727260aca3c141cc17
--- /dev/null
+++ b/tests/syntax/ghost_parameters_formals_status.ml
@@ -0,0 +1,28 @@
+open Cil_types
+
+let run () =
+ let print_info kf =
+ let pretty_formal fmt vi =
+ assert(vi.vformal) ;
+ Format.fprintf fmt "@\n- %a which is %s"
+ Cil_datatype.Varinfo.pretty vi
+ (if vi.vghost then "ghost" else "non-ghost")
+ in
+ let pretty_formal_list fmt l =
+ match l with
+ | [] ->
+ Format.fprintf fmt "No Formals"
+ | _ ->
+ Format.fprintf fmt "Formals are %a"
+ (Pretty_utils.pp_flowlist ~left:"" ~sep:"" ~right:"" pretty_formal) l
+ in
+ let vi = Kernel_function.get_vi kf in
+ let formals = Cil.getFormalsDecl vi in
+ Kernel.feedback "Type of %s is %a.@ %a"
+ vi.vname
+ Cil_datatype.Typ.pretty vi.vtype
+ pretty_formal_list formals
+ in
+ Globals.Functions.iter print_info
+
+let () = Db.Main.extend run
diff --git a/tests/syntax/ghost_parameters_side_effect_arg.i b/tests/syntax/ghost_parameters_side_effect_arg.i
new file mode 100644
index 0000000000000000000000000000000000000000..00d02e6665a1ff8aa1a5cc14d79c76fbcd1fb191
--- /dev/null
+++ b/tests/syntax/ghost_parameters_side_effect_arg.i
@@ -0,0 +1,21 @@
+void function(int x) /*@ ghost(int y) */ ;
+int other(int x) /*@ ghost(int y) */ ;
+
+void caller(){
+ int x = 0 ;
+ //@ ghost int g = 0 ;
+ int t[] = { 0, 0, 0 } ;
+
+ function(x++) /*@ ghost(g++) */ ;
+ function(x = 2) /*@ ghost(g = 42) */ ;
+ function(x += 2) /*@ ghost(g += 42) */ ;
+ function(-x) /*@ ghost(-g) */ ;
+ function( (x == 0) ? x : 42 ) /*@ ghost( (g == 0) ? g : 42 ) */ ;
+ function(t[x++]) /*@ ghost(t[g++]) */ ;
+ function( other(x) /*@ ghost(g) */ ) /*@ ghost( other(x, g) ) */ ;
+
+ /*@ ghost
+ int i = 1 ;
+ function(g++, i++) ;
+ */
+}
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
index 196ad631a7a9bbc1a7f23829cdf4cc367526f137..5d89e874ee4557ea9e97fcec159d21f36e972995 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -6,18 +6,18 @@
/* Generated by Frama-C */
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
-int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
- __f2__, __f1__));
+int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
+(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
+ __f2__, __f1__));
/*@ requires p3 ≥ 3;
requires p3 ≥ 1;
requires p3 ≥ 4; */
-int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
- __f2__, __f1__));
-int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p3)
+int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
+(int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
+ __f2__, __f1__));
+int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f
+(int const __attribute__((__arg3__)) p3)
{
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
__retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
diff --git a/tests/syntax/oracle/ghost_func_ptr.res.oracle b/tests/syntax/oracle/ghost_func_ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..9c2890ad3dc66b42245237d94ea410ff875b9ca5
--- /dev/null
+++ b/tests/syntax/oracle/ghost_func_ptr.res.oracle
@@ -0,0 +1,12 @@
+[kernel] Parsing tests/syntax/ghost_func_ptr.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ ghost void (*g)(int *) = (void (*)(int *))0; */
+int main(void)
+{
+ int __retres;
+ /*@ ghost void (*l)(int *) = (void (*)(int *))0; */
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/ghost_parameters.0.res.oracle b/tests/syntax/oracle/ghost_parameters.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..926c68c1c6b88ab5190ce6d4e0fc0db055e8652e
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.0.res.oracle
@@ -0,0 +1,24 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:29: User Error:
+ Too few ghost arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:30: User Error:
+ Too few ghost arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:31: User Error:
+ Too few arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:32: User Error:
+ Too few ghost arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:32: User Error:
+ Too many arguments in call to function
+[kernel] tests/syntax/ghost_parameters.c:33: User Error:
+ Too many ghost arguments in call to function
+[kernel] tests/syntax/ghost_parameters.c:33: User Error:
+ Too few arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:35: User Error:
+ Too few arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:36: User Error:
+ Too few arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:37: User Error:
+ Too few arguments in call to function.
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.1.res.oracle b/tests/syntax/oracle/ghost_parameters.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..614c8ad74c075c9e1eb74b8277c9cb1dd90ff432
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.1.res.oracle
@@ -0,0 +1,22 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:54: User Error:
+ Too few ghost arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:55: User Error:
+ Too few ghost arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:56: User Error:
+ Too many arguments in call to function
+[kernel] tests/syntax/ghost_parameters.c:57: User Error:
+ Too few ghost arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:57: User Error:
+ Too many arguments in call to function
+[kernel] tests/syntax/ghost_parameters.c:58: User Error:
+ Too many ghost arguments in call to function
+[kernel] tests/syntax/ghost_parameters.c:60: User Error:
+ Too few arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:61: User Error:
+ Too few arguments in call to function.
+[kernel] tests/syntax/ghost_parameters.c:62: User Error:
+ Too many arguments in call to function
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.10.res.oracle b/tests/syntax/oracle/ghost_parameters.10.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..477b266404d4270969128b8295e5957a8ffb1083
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.10.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:184: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:178 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:184: User Error:
+ Inconsistent formals
+ 182 }
+ 183
+ 184 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 185
+ 186 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.11.res.oracle b/tests/syntax/oracle/ghost_parameters.11.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1d8c5da2c6f63a8b566ed678f910648131c852eb
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.11.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:192:
+ syntax error:
+ Location: line 192, between columns 35 and 36, before or at token: )
+ 190 #ifdef VOID_EMPTY_GHOST_PARAMETER_LIST
+ 191
+ 192 void function_void(void) /*@ ghost () */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 193
+ 194 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.12.res.oracle b/tests/syntax/oracle/ghost_parameters.12.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8bc53156a937624d69449742be9e9d452f89dedf
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.12.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:200: User Error:
+ ghost parameters list cannot be void
+[kernel] tests/syntax/ghost_parameters.c:204: User Error:
+ ghost parameters list cannot be void
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.2.res.oracle b/tests/syntax/oracle/ghost_parameters.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..21f52b26feabd38a86fe804f9c8f5ef2033af362
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.2.res.oracle
@@ -0,0 +1,16 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+/* Generated by Frama-C */
+void function(int a, int b) /*@ ghost (int c, int d) */;
+
+void caller(void)
+{
+ function(1,2) /*@ ghost (3,4) */;
+ return;
+}
+
+void function(int a, int b) /*@ ghost (int c, int d) */
+{
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/ghost_parameters.3.res.oracle b/tests/syntax/oracle/ghost_parameters.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..c621d5748d1d6aa8f095a4cb262df1322c86d17d
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.3.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:89: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:85 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:89: User Error:
+ Inconsistent formals
+ 87 }
+ 88
+ 89 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 90
+ 91 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.4.res.oracle b/tests/syntax/oracle/ghost_parameters.4.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d6b376ee2b1e3a910608069d60980a8f0f23dde8
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.4.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:103: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:97 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:103: User Error:
+ Inconsistent formals
+ 101 }
+ 102
+ 103 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 104
+ 105 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.5.res.oracle b/tests/syntax/oracle/ghost_parameters.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..138709d0a9bdc0236cd4021f28304fb0a23c312a
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.5.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:116: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:112 (different number of ghost arguments).
+[kernel] tests/syntax/ghost_parameters.c:116: User Error:
+ Inconsistent formals
+ 114 }
+ 115
+ 116 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 117
+ 118 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.6.res.oracle b/tests/syntax/oracle/ghost_parameters.6.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..5807a9726441f905b6ffed9dd250f8ce4ec425d4
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.6.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:130: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:124 (different number of ghost arguments).
+[kernel] tests/syntax/ghost_parameters.c:130: User Error:
+ Inconsistent formals
+ 128 }
+ 129
+ 130 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 131
+ 132 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.7.res.oracle b/tests/syntax/oracle/ghost_parameters.7.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e5de27561f6b32bb38613b5762dbd2632e2999b4
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.7.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:143: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:139 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:143: User Error:
+ Inconsistent formals
+ 141 }
+ 142
+ 143 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 144
+ 145 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.8.res.oracle b/tests/syntax/oracle/ghost_parameters.8.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..bb6ac89e90999848f2a97340e24f02d246491450
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.8.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:157: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:151 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:157: User Error:
+ Inconsistent formals
+ 155 }
+ 156
+ 157 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 158
+ 159 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.9.res.oracle b/tests/syntax/oracle/ghost_parameters.9.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..53080c4e6f3f5a60ba9ad30cd6a8621da29d5a5d
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters.9.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost_parameters.c (with preprocessing)
+[kernel] tests/syntax/ghost_parameters.c:170: User Error:
+ Declaration of function does not match previous declaration from tests/syntax/ghost_parameters.c:166 (different number of arguments).
+[kernel] tests/syntax/ghost_parameters.c:170: User Error:
+ Inconsistent formals
+ 168 }
+ 169
+ 170 void function(int a, int b) /*@ ghost(int c, int d) */ {
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 171
+ 172 }
+[kernel] User Error: stopping on file "tests/syntax/ghost_parameters.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle b/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f57bed37aaafe5139024b35445d67e4b7a5e1e5a
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters_formals_status.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing tests/syntax/ghost_parameters_formals_status.i (no preprocessing)
+[kernel] Type of caller is void (void).
+ No Formals
+[kernel] Type of declaration_not_void is void (int a, int b)
+ /*@ ghost (int x, int y) */.
+ Formals are
+ - a which is non-ghost
+ - b which is non-ghost
+ - x which is ghost
+ - y which is ghost
+[kernel] Type of declaration_void is void (void) /*@ ghost (int x, int y) */.
+ Formals are
+ - x which is ghost
+ - y which is ghost
+[kernel] Type of definition_not_void is void (int a, int b)
+ /*@ ghost (int x, int y) */.
+ Formals are
+ - a which is non-ghost
+ - b which is non-ghost
+ - x which is ghost
+ - y which is ghost
+[kernel] Type of definition_void is void (void) /*@ ghost (int x, int y) */.
+ Formals are
+ - x which is ghost
+ - y which is ghost
diff --git a/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a74ded6cea571f0de9931b075e58544bef5cdef5
--- /dev/null
+++ b/tests/syntax/oracle/ghost_parameters_side_effect_arg.res.oracle
@@ -0,0 +1,60 @@
+[kernel] Parsing tests/syntax/ghost_parameters_side_effect_arg.i (no preprocessing)
+/* Generated by Frama-C */
+void function(int x) /*@ ghost (int y) */;
+
+int other(int x) /*@ ghost (int y) */;
+
+void caller(void)
+{
+ /*@ ghost int g_tmp; */
+ int tmp;
+ /*@ ghost int g_tmp_0; */
+ int tmp_0;
+ /*@ ghost int g_tmp_1; */
+ int tmp_1;
+ /*@ ghost int g_tmp_2; */
+ int tmp_2;
+ /*@ ghost int g_tmp_3; */
+ /*@ ghost int g_tmp_4; */
+ int x = 0;
+ /*@ ghost int g = 0; */
+ int t[3] = {0, 0, 0};
+ /*@ ghost g_tmp = g; */
+ /*@ ghost g ++; */
+ /*@ ghost ; */
+ tmp = x;
+ x ++;
+ ;
+ function(tmp) /*@ ghost (g_tmp) */;
+ /*@ ghost g = 42; */
+ x = 2;
+ function(x) /*@ ghost (g) */;
+ /*@ ghost g += 42; */
+ x += 2;
+ function(x) /*@ ghost (g) */;
+ function(- x) /*@ ghost (- g) */;
+ /*@ ghost if (g == 0) g_tmp_0 = g; else g_tmp_0 = 42; */
+ if (x == 0) tmp_0 = x; else tmp_0 = 42;
+ function(tmp_0) /*@ ghost (g_tmp_0) */;
+ /*@ ghost g_tmp_1 = g; */
+ /*@ ghost g ++; */
+ /*@ ghost ; */
+ tmp_1 = x;
+ x ++;
+ ;
+ function(t[tmp_1]) /*@ ghost (t[g_tmp_1]) */;
+ /*@ ghost g_tmp_2 = other(x,g); */
+ tmp_2 = other(x) /*@ ghost (g) */;
+ function(tmp_2) /*@ ghost (g_tmp_2) */;
+ /*@ ghost int i = 1; */
+ /*@ ghost g_tmp_3 = i;
+ i ++;
+ ;
+ g_tmp_4 = g;
+ g ++;
+ ; */
+ /*@ ghost function(g_tmp_4,g_tmp_3); */
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/undeclared_local_bts1126.res.oracle b/tests/syntax/oracle/undeclared_local_bts1126.res.oracle
index c1237aab0ad82b4be7420cc870484c8c1a324622..4c135cc183f7d23101b0de47587639afbbcd88f0 100644
--- a/tests/syntax/oracle/undeclared_local_bts1126.res.oracle
+++ b/tests/syntax/oracle/undeclared_local_bts1126.res.oracle
@@ -32,8 +32,8 @@ extern int ( /* missing proto */ _gnutls_epoch_get)(struct gnutls_session_t x_0,
extern int ( /* missing proto */ gnutls_assert_val)(int x_0);
-extern int ( /* missing proto */ _gnutls_cipher_suite_get_cipher_algo)(
-cipher_suite_st *x_0);
+extern int ( /* missing proto */ _gnutls_cipher_suite_get_cipher_algo)
+(cipher_suite_st *x_0);
extern int ( /* missing proto */ _gnutls_cipher_suite_get_mac_algo)(cipher_suite_st *x_0);