Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Test 32-bit builds in CI and fix platform-specific code and tests #7756

Merged
merged 19 commits into from
Sep 22, 2023
Merged
Changes from 1 commit
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
24d4d3a
Fix 32bit unit test build failure
tautschnig Jun 6, 2023
37ed69c
Unit tests: do not hard-code 64-bit pointer width
tautschnig Jul 7, 2023
caca58b
Interpreter: Do not hard-code platform bit width
tautschnig Aug 2, 2023
093e2f3
Make goto-inspect test patterns platform-agnostic
tautschnig Aug 2, 2023
352299a
Test patterns: fix optional casts
tautschnig Aug 2, 2023
3318f6f
goto-harness regression tests: support non-64-bit platforms
tautschnig Aug 2, 2023
ebaf09f
Arrays have a signed size
tautschnig Aug 2, 2023
a9ca74e
Fix tests and contracts wrongly assuming sizeof(long) == sizeof(long …
tautschnig Aug 2, 2023
0723271
Tests: use types that are smaller than long on all platforms
tautschnig Aug 2, 2023
ba7eb04
Tests: do not hard-code 64 bits/8 bytes as pointer width
tautschnig Aug 2, 2023
a3f1ae9
Tests: fix index typo
tautschnig Aug 2, 2023
28e4238
Properly type initial value of __CPROVER_max_malloc_size
tautschnig Aug 7, 2023
5eb8a94
Goto analyzer: do not create untyped nil expression
tautschnig Aug 7, 2023
cc27808
Make cbmc-incr-smt2 test patterns platform-agnostic
tautschnig Aug 8, 2023
9d1be21
cbmc-incr-smt2 tests: remove misguided assertion
tautschnig Aug 8, 2023
0794f5b
Incremental SMT2: support cast from pointer to integer of different w…
tautschnig Aug 8, 2023
c1f9237
Make memory-analyzer compatible with i386
tautschnig Aug 8, 2023
1cae1b3
Contracts test: ensure return value access is in bounds
tautschnig Aug 8, 2023
1a30ad4
Run 32-bit builds and tests as CI job
tautschnig Jun 6, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Make goto-inspect test patterns platform-agnostic
Not all platforms have 32-bit int, and the size of long int may be the
same as int.
tautschnig committed Aug 23, 2023
commit 093e2f30435b89c06b5a4e33310b9c26b381a2bf
4 changes: 2 additions & 2 deletions regression/goto-inspect/show-goto-functions/positive.desc
Original file line number Diff line number Diff line change
@@ -4,9 +4,9 @@ main.c
^EXIT=0$
^SIGNAL=0$
main
DECL main::1::arr : signedbv\[32\]\[5\]
DECL main::1::arr : signedbv\[\d+\]\[5\]
ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \}
ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0
ASSERT main::1::arr\[(0|cast\(0, signedbv\[\d+\]\))\] ≠ 0 // Expected failure: 0 == 0
DEAD main::1::arr
SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1"
END_FUNCTION