diff --git a/.Makefile.lint b/.Makefile.lint
index fc916bfa1e33d42ff2e73b588b496e21b2d85da4..c74c7c5be984e086ae376f259a784e7374c0f3e5 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -11,8 +11,6 @@ ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
-ML_LINT_KO+=src/kernel_internals/typing/alpha.ml
-ML_LINT_KO+=src/kernel_internals/typing/alpha.mli
ML_LINT_KO+=src/kernel_internals/typing/asm_contracts.ml
ML_LINT_KO+=src/kernel_internals/typing/cfg.ml
ML_LINT_KO+=src/kernel_internals/typing/cfg.mli
diff --git a/src/kernel_internals/typing/alpha.ml b/src/kernel_internals/typing/alpha.ml
index fd3269331a1a6b664535e977fc0f4580daecb633..727d2c77733d52b85bd88b6e909f69f36e46f6a5 100644
--- a/src/kernel_internals/typing/alpha.ml
+++ b/src/kernel_internals/typing/alpha.ml
@@ -47,16 +47,16 @@ module H = Hashtbl
let alphaSeparator = '_'
(** For each prefix we remember the last integer suffix that has been used
- (to start searching for a fresh name) and the list
- * of suffixes, each with some data associated with the newAlphaName that
+ (to start searching for a fresh name) and the list
+ * of suffixes, each with some data associated with the newAlphaName that
* created the suffix. *)
type 'a alphaTableData = Integer.t * (Integer.t * 'a) list
-type 'a undoAlphaElement =
- AlphaChangedSuffix of 'a alphaTableData ref * 'a alphaTableData (* The
- * reference that was changed and
- * the old suffix *)
- | AlphaAddedSuffix of string * string (* We added this new entry to the
+type 'a undoAlphaElement =
+ AlphaChangedSuffix of 'a alphaTableData ref * 'a alphaTableData (* The
+ * reference that was changed and
+ * the old suffix *)
+ | AlphaAddedSuffix of string * string (* We added this new entry to the
* table *)
type 'a alphaTable = (string, (string, 'a alphaTableData ref) H.t) H.t
@@ -64,11 +64,11 @@ type 'a alphaTable = (string, (string, 'a alphaTableData ref) H.t) H.t
(* specify a behavior for renaming *)
type rename_mode =
| Incr_last_suffix
- (* increment the last suffix in the original id
- (adding _nnn if no suffix exists in the original id) *)
+ (* increment the last suffix in the original id
+ (adding _nnn if no suffix exists in the original id) *)
| Add_new_suffix
- (* systematically adds a _nnn suffix even if the original name
- ends with _mmm *)
+ (* systematically adds a _nnn suffix even if the original name
+ ends with _mmm *)
let has_generated_prefix n prefix =
let prefix_length = String.length prefix in
@@ -79,39 +79,39 @@ let has_generated_prefix n prefix =
end else n
in
String.length real_name >= prefix_length &&
- String.sub real_name 0 prefix_length = prefix
+ String.sub real_name 0 prefix_length = prefix
let generated_prefixes = [ "__anon"; "__constr_expr" ]
let is_generated_name n =
List.exists (has_generated_prefix n) generated_prefixes
-(* Strip the suffix. Return the prefix, the suffix (including the separator
- * but not the numeric value, possibly empty), and the
- * numeric value of the suffix (possibly -1 if missing) *)
-let splitNameForAlpha ~(lookupname: string) =
+(* Strip the suffix. Return the prefix, the suffix (including the separator
+ * but not the numeric value, possibly empty), and the
+ * numeric value of the suffix (possibly -1 if missing) *)
+let splitNameForAlpha ~(lookupname: string) =
let len = String.length lookupname in
- (* Search backward for the numeric suffix. Return the first digit of the
+ (* Search backward for the numeric suffix. Return the first digit of the
* suffix. Returns len if no numeric suffix *)
let rec skipSuffix seen_sep last_sep (i: int) =
if i = -1 then last_sep else
- let c = lookupname.[i] in
- (* we might start to use Str at some point. *)
- if (Char.compare '0' c <= 0 && Char.compare c '9' <= 0) then
- skipSuffix false last_sep (i - 1)
- else if c = alphaSeparator then
- if not seen_sep then
- (* check whether we are in the middle of a multi-suffix ident
- e.g. x_0_2, where the prefix would be x. *)
- skipSuffix true i (i-1)
- else (* we have something like x__0. Consider x_ as the prefix. *)
- i+1
- else (* we have something like x1234_0. Consider x1234 as the prefix *)
- last_sep
+ let c = lookupname.[i] in
+ (* we might start to use Str at some point. *)
+ if (Char.compare '0' c <= 0 && Char.compare c '9' <= 0) then
+ skipSuffix false last_sep (i - 1)
+ else if c = alphaSeparator then
+ if not seen_sep then
+ (* check whether we are in the middle of a multi-suffix ident
+ e.g. x_0_2, where the prefix would be x. *)
+ skipSuffix true i (i-1)
+ else (* we have something like x__0. Consider x_ as the prefix. *)
+ i+1
+ else (* we have something like x1234_0. Consider x1234 as the prefix *)
+ last_sep
in
(* we start as if the next char of the identifier was _, so that
x123_ is seen as a prefix.
- *)
+ *)
let startSuffix = skipSuffix true len (len - 1) in
if startSuffix >= len
then
@@ -129,11 +129,11 @@ let make_full_suffix infix n = infix ^ make_suffix n
elements of l are less than or equal to max.
returns the new suffix and a new bound to max in case the new suffix is
greater than max.
- *)
+*)
let find_unused_suffix min infix sibling l =
let rec aux v =
if List.exists (fun (n,_) -> Integer.equal n v) l
- || H.mem sibling (make_full_suffix infix v)
+ || H.mem sibling (make_full_suffix infix v)
then begin
Kernel.debug ~dkey:Kernel.dkey_alpha
"%s is already taken" (make_full_suffix infix v);
@@ -143,27 +143,27 @@ let find_unused_suffix min infix sibling l =
let get_suffix_idx rename_mode infix =
match rename_mode with
- | Add_new_suffix -> infix, Integer.minus_one
- | Incr_last_suffix when infix = "" -> infix, Integer.minus_one
- | Incr_last_suffix ->
- (* by construction there is at least one alphaSeparator in the infix *)
- let idx = String.rindex infix alphaSeparator in
- String.sub infix 0 idx,
- Integer.of_string
- (String.sub infix (idx + 1) (String.length infix - idx - 1))
+ | Add_new_suffix -> infix, Integer.minus_one
+ | Incr_last_suffix when infix = "" -> infix, Integer.minus_one
+ | Incr_last_suffix ->
+ (* by construction there is at least one alphaSeparator in the infix *)
+ let idx = String.rindex infix alphaSeparator in
+ String.sub infix 0 idx,
+ Integer.of_string
+ (String.sub infix (idx + 1) (String.length infix - idx - 1))
-(* Create a new name based on a given name. The new name is formed from a
- * prefix (obtained from the given name by stripping a suffix consisting of
- * the alphaSeparator followed by only digits), followed by alphaSeparator
- * and then by a positive integer suffix. The first argument is a table
- * mapping name prefixes to the largest suffix used so far for that
- * prefix. The largest suffix is one when only the version without suffix has
+(* Create a new name based on a given name. The new name is formed from a
+ * prefix (obtained from the given name by stripping a suffix consisting of
+ * the alphaSeparator followed by only digits), followed by alphaSeparator
+ * and then by a positive integer suffix. The first argument is a table
+ * mapping name prefixes to the largest suffix used so far for that
+ * prefix. The largest suffix is one when only the version without suffix has
* been used. *)
let alphaWorker ~(alphaTable: 'a alphaTable)
- ?undolist
- ~(lookupname: string) ~(data:'a)
- (make_new: bool) : string * 'a =
+ ?undolist
+ ~(lookupname: string) ~(data:'a)
+ (make_new: bool) : string * 'a =
let prefix, infix = splitNameForAlpha ~lookupname in
let rename_mode =
if is_generated_name prefix then Incr_last_suffix else Add_new_suffix
@@ -179,63 +179,66 @@ let alphaWorker ~(alphaTable: 'a alphaTable)
let min, suffixes = !rc in
(* We have seen this prefix *)
Kernel.debug ~dkey:Kernel.dkey_alpha "Old min %s. Old suffixes: @[%a@]"
- (Integer.to_string min)
+ (Integer.to_string min)
(Pretty_utils.pp_list
(fun fmt (s,_) -> Format.fprintf fmt "%s" (Integer.to_string s)))
suffixes;
(* Save the undo info *)
(match undolist with
- Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l
- | _ -> ());
+ Some l -> l := AlphaChangedSuffix (rc, !rc) :: !l
+ | _ -> ());
let newname, newmin, (olddata: 'a), newsuffixes =
match
List.filter (fun (n, _) -> Integer.equal n curr_idx) suffixes
with
- | [] -> (* never seen this index before *)
- lookupname, min, data, (curr_idx, data) :: suffixes
- | [(_, l) ] ->
- (* We have seen this exact suffix before *)
- (* In Incr_last_suffix mode, we do not take curr_idx into account,
- but select the first available index available *)
- if make_new then begin
- let newmin =
- find_unused_suffix (Integer.succ min) infix infixes suffixes
- in
- let newsuffix = make_suffix newmin in
- let base =
- if is_generated_name prefix then prefix else lookupname
- in
- H.add
- infixes newsuffix
- (ref (Integer.minus_one, [(Integer.minus_one, data)]));
- (match undolist with
- | Some l -> l:= AlphaAddedSuffix (prefix,newsuffix)::!l
- | None -> ());
- base ^ newsuffix, newmin, l, (newmin, data) :: suffixes
- end else lookupname, min, data, suffixes
- | _ -> (Kernel.fatal "Cil.alphaWorker")
+ | [] -> (* never seen this index before *)
+ lookupname, min, data, (curr_idx, data) :: suffixes
+ | [(_, l) ] ->
+ (* We have seen this exact suffix before *)
+ (* In Incr_last_suffix mode, we do not take curr_idx into account,
+ but select the first available index available *)
+ if make_new then begin
+ let newmin =
+ find_unused_suffix (Integer.succ min) infix infixes suffixes
+ in
+ let newsuffix = make_suffix newmin in
+ let newinfix = make_full_suffix infix newmin in
+ Kernel.(
+ debug ~dkey:dkey_alpha "New suffix: %s" newsuffix);
+ let base =
+ if is_generated_name prefix then prefix else lookupname
+ in
+ H.add
+ infixes newinfix
+ (ref (Integer.minus_one, [(Integer.minus_one, data)]));
+ (match undolist with
+ | Some l -> l:= AlphaAddedSuffix (prefix,newsuffix)::!l
+ | None -> ());
+ base ^ newsuffix, newmin, l, (newmin, data) :: suffixes
+ end else lookupname, min, data, suffixes
+ | _ -> (Kernel.fatal "Cil.alphaWorker")
in
rc := (newmin, newsuffixes);
newname, olddata
with Not_found -> begin (* First variable with this prefix *)
- (match undolist with
- Some l -> l := AlphaAddedSuffix (prefix,infix) :: !l
- | _ -> ());
- let infixes =
- try H.find alphaTable prefix
- with Not_found ->
- let h = H.create 3 in H.add alphaTable prefix h; h
- in
- H.add infixes infix
- (ref (Integer.minus_one, [ (curr_idx, data) ]));
- Kernel.debug ~dkey:Kernel.dkey_alpha " First seen. ";
- lookupname, data (* Return the original name *)
- end
+ (match undolist with
+ Some l -> l := AlphaAddedSuffix (prefix,infix) :: !l
+ | _ -> ());
+ let infixes =
+ try H.find alphaTable prefix
+ with Not_found ->
+ let h = H.create 3 in H.add alphaTable prefix h; h
+ in
+ H.add infixes infix
+ (ref (Integer.minus_one, [ (curr_idx, data) ]));
+ Kernel.debug ~dkey:Kernel.dkey_alpha " First seen. ";
+ lookupname, data (* Return the original name *)
+ end
in
Kernel.debug ~dkey:Kernel.dkey_alpha "Res=: %s" newname;
newname, olddata
-
+
let newAlphaName ~alphaTable ?undolist ~lookupname ~data =
alphaWorker ~alphaTable ?undolist ~lookupname ~data true
@@ -246,11 +249,11 @@ let registerAlphaName ~alphaTable ?undolist ~lookupname ~data =
let getAlphaPrefix ~lookupname = splitNameForAlpha ~lookupname
(* Undoes the changes as specified by the undolist *)
-let undoAlphaChanges ~alphaTable ~undolist =
+let undoAlphaChanges ~alphaTable ~undolist =
List.iter
- (function
- AlphaChangedSuffix (where, old) ->
- where := old
+ (function
+ AlphaChangedSuffix (where, old) ->
+ where := old
| AlphaAddedSuffix (prefix, infix) ->
Kernel.debug ~dkey:Kernel.dkey_alpha_undo
"Removing %s%s from alpha table\n" prefix infix;
@@ -263,4 +266,3 @@ let undoAlphaChanges ~alphaTable ~undolist =
"prefix %s has no entry in the table. Inconsistent undo list"
prefix)
undolist
-
diff --git a/src/kernel_internals/typing/alpha.mli b/src/kernel_internals/typing/alpha.mli
index 852b6791ab4784f1b6f0fb05e8867759e8199015..9101266f4187f9bad0896d686939301ff27b8c3b 100644
--- a/src/kernel_internals/typing/alpha.mli
+++ b/src/kernel_internals/typing/alpha.mli
@@ -43,52 +43,52 @@
(** Alpha conversion. *)
-(** This is the type of the elements that are recorded by the alpha
- * conversion functions in order to be able to undo changes to the tables
- * they modify. Useful for implementing
+(** This is the type of the elements that are recorded by the alpha
+ * conversion functions in order to be able to undo changes to the tables
+ * they modify. Useful for implementing
* scoping *)
type 'a undoAlphaElement
-(** This is the type of the elements of the alpha renaming table. These
+(** This is the type of the elements of the alpha renaming table. These
* elements can carry some data associated with each occurrence of the name. *)
type 'a alphaTableData
(** type for alpha conversion table. We split the lookup in two to avoid
creating accidental collisions when converting x_0 into x_0_0 if the
original code contains both. *)
-type 'a alphaTable =
+type 'a alphaTable =
(string, (string, 'a alphaTableData ref) Hashtbl.t) Hashtbl.t
-(** Create a new name based on a given name. The new name is formed from a
- * prefix (obtained from the given name by stripping a suffix consisting of _
- * followed by only digits), followed by a special separator and then by a
- * positive integer suffix. The first argument is a table mapping name
- * prefixes to some data that specifies what suffixes have been used and how
- * to create the new one. This function updates the table with the new
- * largest suffix generated. The "undolist" argument, when present, will be
- * used by the function to record information that can be used by
- * {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo
- * information will be in reverse order in which the action occurred. Returns
- * the new name and, if different from the lookupname, the location of the
- * previous occurrence. This function knows about the location implicitly
+(** Create a new name based on a given name. The new name is formed from a
+ * prefix (obtained from the given name by stripping a suffix consisting of _
+ * followed by only digits), followed by a special separator and then by a
+ * positive integer suffix. The first argument is a table mapping name
+ * prefixes to some data that specifies what suffixes have been used and how
+ * to create the new one. This function updates the table with the new
+ * largest suffix generated. The "undolist" argument, when present, will be
+ * used by the function to record information that can be used by
+ * {!Alpha.undoAlphaChanges} to undo those changes. Note that the undo
+ * information will be in reverse order in which the action occurred. Returns
+ * the new name and, if different from the lookupname, the location of the
+ * previous occurrence. This function knows about the location implicitly
* from the [(Cil.CurrentLoc.get ())]. *)
val newAlphaName: alphaTable: 'a alphaTable ->
- ?undolist: 'a undoAlphaElement list ref ->
- lookupname:string -> data:'a -> string * 'a
+ ?undolist: 'a undoAlphaElement list ref ->
+ lookupname:string -> data:'a -> string * 'a
-(** Register a name with an alpha conversion table to ensure that when later
+(** Register a name with an alpha conversion table to ensure that when later
* we call newAlphaName we do not end up generating this one *)
val registerAlphaName: alphaTable: 'a alphaTable ->
- ?undolist: 'a undoAlphaElement list ref ->
- lookupname:string -> data:'a -> unit
+ ?undolist: 'a undoAlphaElement list ref ->
+ lookupname:string -> data:'a -> unit
-(** Split the name in preparation for newAlphaName. Returns a pair
+(** Split the name in preparation for newAlphaName. Returns a pair
[(prefix, infix)] where [prefix] is the index in the outer table, while
infix is the index in the inner table.
*)
val getAlphaPrefix: lookupname:string -> string * string
(** Undo the changes to a table *)
-val undoAlphaChanges: alphaTable:'a alphaTable ->
- undolist:'a undoAlphaElement list -> unit
+val undoAlphaChanges: alphaTable:'a alphaTable ->
+ undolist:'a undoAlphaElement list -> unit
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index b72e5035f8292f7be0520c3245b0d4a5af28158a..a66624a0fd68623c39c61a95fa1ae66b0a92110d 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -867,9 +867,7 @@ let remove_label_env lab =
* hash table easily *)
type undoScope =
UndoRemoveFromEnv of string
- | UndoResetAlphaCounter of location Alpha.alphaTableData ref *
- location Alpha.alphaTableData
- | UndoRemoveFromAlphaTable of string * string
+ | UndoAlphaEnv of location Alpha.undoAlphaElement list
let scopes : undoScope list ref list ref = ref []
@@ -881,14 +879,10 @@ let declared_in_current_scope s =
| cur_scope :: _ ->
let names_declared_in_current_scope =
Extlib.filter_map
- (fun us ->
- match us with
- | UndoRemoveFromEnv _ | UndoRemoveFromAlphaTable _ -> true
- | UndoResetAlphaCounter _ -> false)
- (fun us ->
- match us with
- | UndoRemoveFromEnv s | UndoRemoveFromAlphaTable (s,_) -> s
- | UndoResetAlphaCounter _ -> assert false (* already filtered *)
+ (function UndoRemoveFromEnv _ -> true | UndoAlphaEnv _ -> false)
+ (function
+ | UndoRemoveFromEnv s -> s
+ | UndoAlphaEnv _ -> assert false (* already filtered *)
) !cur_scope
in
List.mem s names_declared_in_current_scope
@@ -973,29 +967,24 @@ let newAlphaName (globalscope: bool) (* The name should have global scope *)
* the top-most scope (that of the enclosing function) *)
let rec findEnclosingFun = function
[] -> (* At global scope *) None
- | [s] -> begin
- let prefix, infix = Alpha.getAlphaPrefix lookupname in
- try
- let infixes = H.find alphaTable prefix in
- let countref = H.find infixes infix in
- s := (UndoResetAlphaCounter (countref, !countref)) :: !s; Some s
- with Not_found ->
- s := (UndoRemoveFromAlphaTable (prefix, infix)) :: !s; Some s;
- end
+ | [s] -> Some s
| _ :: rest -> findEnclosingFun rest
in
let undo_scope =
if not globalscope then findEnclosingFun !scopes else None
in
+ let undolist =
+ match undo_scope with None -> None | Some _ -> Some (ref [])
+ in
+ let data = CurrentLoc.get () in
let newname, oldloc =
- Alpha.newAlphaName alphaTable lookupname (CurrentLoc.get ())
+ Alpha.newAlphaName ~alphaTable ?undolist ~lookupname ~data
in
+ (match undo_scope, undolist with
+ | None, None -> ()
+ | Some s, Some l -> s := (UndoAlphaEnv !l) :: !s
+ | _ -> assert false (* by construction, both options have the same status*));
if newname <> lookupname then begin
- (match undo_scope with
- | None -> ()
- | Some s ->
- let newpre, newinf = Alpha.getAlphaPrefix newname in
- s := (UndoRemoveFromAlphaTable (newpre, newinf)) :: !s);
try
let info =
if !scopes = [] then begin
@@ -3840,18 +3829,8 @@ let exitScope () =
[] -> ()
| UndoRemoveFromEnv n :: t ->
H.remove env n; loop t
- | UndoRemoveFromAlphaTable (p,i) :: t ->
- (try
- let h = H.find alphaTable p in
- H.remove h i;
- if H.length h = 0 then H.remove alphaTable p
- with Not_found ->
- Kernel.warning
- "prefix (%s,%s) not in alpha conversion table. \
- undo stack is inconsistent"
- p i); loop t
- | UndoResetAlphaCounter (vref, oldv) :: t ->
- vref := oldv;
+ | UndoAlphaEnv undolist :: t ->
+ Alpha.undoAlphaChanges ~alphaTable ~undolist;
loop t
in
loop !this;
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index c5e01b7134df44a227c6d801e2ab9e1e6f2c0da0..6ce13b9bca6b0e30e6afd22fc88a9f2901006c7f 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -7444,7 +7444,9 @@ let isCompleteType ?allowZeroSizeArrays t =
let undolist = ref [] in
(* Process one local variable *)
let processLocal (v: varinfo) =
- let lookupname = v.vname in
+ (* start from original name to avoid putting another _0 in case
+ of conflicts. *)
+ let lookupname = v.vorig_name in
let data = CurrentLoc.get () in
let newname, oldloc =
Alpha.newAlphaName
diff --git a/tests/spec/oracle/array_typedef.res.oracle b/tests/spec/oracle/array_typedef.res.oracle
index f70e7649412bf74a7c3ba31a62b99f88f3cf497d..51da3e81b847059d1e847ddc3d83ac4ff39b6b75 100644
--- a/tests/spec/oracle/array_typedef.res.oracle
+++ b/tests/spec/oracle/array_typedef.res.oracle
@@ -73,9 +73,9 @@ typedef struct __anonstruct_msg_1 msg;
/*@ assigns \empty; */
void send_addr(int const * /*[4]*/ addr);
-void send_msg(msg const *msg_0)
+void send_msg(msg const *msg)
{
- send_addr(msg_0->src);
+ send_addr(msg->src);
return;
}
@@ -89,13 +89,13 @@ void host_address(int * /*[4]*/ ip)
return;
}
-void create_msg(msg *msg_0)
+void create_msg(msg *msg)
{
- host_address(msg_0->src);
- host_address(msg_0->dst);
- /*@ assert msg_0->dst[0] ≡ 192; */ ;
- /*@ assert msg_0->src[0] ≡ 192; */ ;
- /*@ assert msg_0->dst[sizeof(ip_address) / sizeof(int) - 1] ≡ 101; */ ;
+ host_address(msg->src);
+ host_address(msg->dst);
+ /*@ assert msg->dst[0] ≡ 192; */ ;
+ /*@ assert msg->src[0] ≡ 192; */ ;
+ /*@ assert msg->dst[sizeof(ip_address) / sizeof(int) - 1] ≡ 101; */ ;
return;
}
diff --git a/tests/spec/oracle/sizeof_logic.res.oracle b/tests/spec/oracle/sizeof_logic.res.oracle
index 0bc5ea119a70b054dcd245edb0d966a3d446217d..a5f76a76a31a84dd0b3e5437945eb724c26c616a 100644
--- a/tests/spec/oracle/sizeof_logic.res.oracle
+++ b/tests/spec/oracle/sizeof_logic.res.oracle
@@ -10,7 +10,7 @@ struct S {
/*@ lemma good: ∀ short x; sizeof(x) ≤ sizeof(int);
*/
/*@ ensures \result ≡ sizeof(struct S volatile); */
-int f(int a_0)
+int f(int a)
{
int __retres;
__retres = (int)sizeof(struct S volatile);
diff --git a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
index 57fdf7c199509f4598052b6bda6914f92e5934f4..40ab5bd3e4c647a6c27382809667e8c55a56a5e6 100644
--- a/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
+++ b/tests/syntax/oracle/attributes-declarations-definitions.res.oracle
@@ -7,20 +7,20 @@
typedef int __attribute__((__a1__)) aint;
typedef int __attribute__((__p1__)) * __attribute__((__p2__)) iptr;
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4) __attribute__((__f5__, __f4__,
+int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
__f2__, __f1__));
-/*@ requires p4 ≥ 3;
- requires p4 ≥ 1;
- requires p4 ≥ 4; */
+/*@ requires p3 ≥ 3;
+ requires p3 ≥ 1;
+ requires p3 ≥ 4; */
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4) __attribute__((__f5__, __f4__,
+int const __attribute__((__arg3__)) p3) __attribute__((__f5__, __f4__,
__f2__, __f1__));
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) f(
-int const __attribute__((__arg3__)) p4)
+int const __attribute__((__arg3__)) p3)
{
int __attribute__((__tret5__, __tret4__, __tret3__, __tret2__, __tret1__)) __retres;
- __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p4;
+ __retres = (int __attribute__((__tret3__, __tret2__, __tret1__)))p3;
return __retres;
}
@@ -33,9 +33,9 @@ aint g(int __attribute__((__a2__)) i3)
return __retres;
}
-iptr h(iptr volatile ip3);
+iptr h(iptr volatile ip2);
-iptr h(iptr volatile ip3)
+iptr h(iptr volatile ip2)
{
iptr __retres;
__retres = (int __attribute__((__p1__)) *)0;
diff --git a/tests/syntax/oracle/bts0588.res.oracle b/tests/syntax/oracle/bts0588.res.oracle
index 974690514254374dffaeac43e79345266621c961..1bb974c5380efd6ae747bdeb7d28fbda1385ff21 100644
--- a/tests/syntax/oracle/bts0588.res.oracle
+++ b/tests/syntax/oracle/bts0588.res.oracle
@@ -8,10 +8,10 @@ void g(int a)
return;
}
-/*@ ensures \old(x) > 0; */
-void f(int x)
+/*@ ensures \old(a) > 0; */
+void f(int a)
{
- x = 1;
+ a = 1;
return;
}
diff --git a/tests/syntax/oracle/rename.res.oracle b/tests/syntax/oracle/rename.res.oracle
index 52e6869da0887ef55a31547b8483fa061a1024d4..3014a97f9301faebbaaabe955ae4752894f09e65 100644
--- a/tests/syntax/oracle/rename.res.oracle
+++ b/tests/syntax/oracle/rename.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/syntax/rename.i (no preprocessing)
-[kernel] tests/syntax/rename.i:48: Warning:
+[kernel] tests/syntax/rename.i:69: Warning:
unnamed fields are a C11 extension (use -c11 to avoid this warning)
/* Generated by Frama-C */
struct not_anon {
@@ -73,6 +73,32 @@ void f4(int *j_0_1)
return;
}
+void f5(void)
+{
+ int y_0_1;
+ int y_0_0;
+ return;
+}
+
+int y_0;
+void f6(void)
+{
+ int y_2_0;
+ int y_2;
+ return;
+}
+
+int y_1;
+void f7(void)
+{
+ {
+ int __constr_expr_1 = 0;
+ }
+ int __constr_expr_2 = 0;
+ return;
+}
+
+int __constr_expr_0 = 0;
struct not_anon s = {.__anonCompField1 = 0};
struct anon a = {.__anonCompField1 = {.inner_i = 0}};
diff --git a/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle b/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
index dac79fa8c28ed0d122f90ee83dc0ac7e7dd0a8f9..d1362720e3451b7c18a430bd0a496fe5447c5ae8 100644
--- a/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
+++ b/tests/syntax/oracle/typedef_namespace_bts1500.0.res.oracle
@@ -9,8 +9,8 @@ int main(void)
{
int __retres;
digit x = 4;
- int digit_0 = 3;
- __retres = (x + digit_0) + A;
+ int digit = 3;
+ __retres = (x + digit) + A;
return __retres;
}
diff --git a/tests/syntax/rename.i b/tests/syntax/rename.i
index 08a549ccc24c4a4c1d072dcbc7046321a8da60e6..053c6546f7736200c0d12669e59e9fd35713109f 100644
--- a/tests/syntax/rename.i
+++ b/tests/syntax/rename.i
@@ -39,6 +39,27 @@ void f4(int *j_0_1) {
j_0_1+=j_0; }
}
+void f5() {
+ { int y_0; }
+ int y_0;
+}
+
+int y_0;
+
+void f6() {
+ { int y_2; }
+ int y_2;
+}
+
+int y_1;
+
+void f7() {
+ { int __constr_expr_1 = 0; }
+ int __constr_expr_1 = 0;
+}
+
+int __constr_expr_0 = 0;
+
struct not_anon {
int __anonCompField1;
};