Skip to content

Commit

Permalink
Merge pull request #157 from goblint/builtin_types_compatible
Browse files Browse the repository at this point in the history
Ignore top level qualifiers in `__builtin_types_compatible_p`
  • Loading branch information
karoliineh authored Oct 3, 2023
2 parents 44f156c + cd07bb1 commit 13efd21
Show file tree
Hide file tree
Showing 3 changed files with 13 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/frontc/cabs2cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4658,7 +4658,8 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
prechunk := (fun _ -> empty);
piscall := false;
let compatible =
try ignore(combineTypes CombineOther t1 t2); true
(* This built-in function ignores top level qualifiers (e.g., const, volatile). *)
try ignore(combineTypes CombineOther (removeOuterQualifierAttributes t1) (removeOuterQualifierAttributes t2)); true
with Failure _ -> false
in
if compatible then
Expand Down
10 changes: 10 additions & 0 deletions test/small1/builtin6.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@

// Extracted from the git repository.
// CIL used to crash with "Error: Length of array is negative".

int main() {
const int *a;
int *ret;
sizeof(*(ret)) + (sizeof(char [1 - 2*!(__builtin_types_compatible_p(__typeof__(*((ret))), __typeof__(*((a)))))]) - 1);
return 0;
}
1 change: 1 addition & 0 deletions test/testcil.pl
Original file line number Diff line number Diff line change
Expand Up @@ -548,6 +548,7 @@ sub addToGroup {
addTest("testrungcc/builtin_object_size _GNUCC=1 OPTIMIZE=1");
addTest("testrun/builtin4 ");
addTest("test/builtin5 ");
addTest("test/builtin6 ");
addTest("test/sync-1 _GNUCC=1");
addTest("test/sync-2 _GNUCC=1");
addTest("test/sync-3 _GNUCC=1");
Expand Down

0 comments on commit 13efd21

Please sign in to comment.