-
Notifications
You must be signed in to change notification settings - Fork 260
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
New option --mmio-regions to specify memory regions
This new option will enable us to eventually drop support for __CPROVER_allocated_memory, which 1) requires awkward scanning of goto functions in goto_check_c, 2) wrongly suggests these declarations are limited to some scope, and 3) yields a spurious undefined-function warning in symex.
- Loading branch information
1 parent
365871d
commit fafe18a
Showing
7 changed files
with
60 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
CORE broken-smt-backend | ||
main.c | ||
--pointer-check -DCMDLINE --mmio-regions 0x10:4 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[main\.pointer_dereference\.2\] .* dereference failure: invalid integer address in \*p: SUCCESS$ | ||
^\[main\.assertion\.1\] .* assertion \*p==42: SUCCESS$ | ||
^\[main\.pointer_dereference\.[0-9]+\] .* dereference failure: invalid integer address in p\[.*1\]: FAILURE$ | ||
^\[main\.assertion\.2\] .* assertion \*\(p\+1\)==42: SUCCESS$ | ||
^VERIFICATION FAILED$ | ||
-- | ||
^warning: ignoring |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
CORE | ||
main.c | ||
--bounds-check -DCMDLINE --mmio-regions 0x1000:400,0x11000:400 --mmio-regions 0x21000:400,0x31000:400 | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ | ||
^\[main\.array_bounds\.[67]\] line 40 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ | ||
^\*\* 1 of 12 failed | ||
^VERIFICATION FAILED$ | ||
-- | ||
^warning: ignoring |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters