Fix graphml output of concurrency witnesses #1511
Merged
Conversation
This file contains hidden or 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
The START_THREAD instruction may induce a number of assignments, which end up as assignment in the symex_target_equation while the corresponding pc still points to a START_THREAD instruction. Hence testing assignments must be done consistently either within the symex_target_equation or within the goto program level.
tautschnig
requested review from
kroening,
peterschrammel and
smowton
as code owners
smowton
approved these changes
Oct 24, 2017
|
|
||
| int main() | ||
| { | ||
| __CPROVER_ASYNC_1: global=1; |
There was a problem hiding this comment.
Suggest // Create thread to set global to 1 then exit
| int main() | ||
| { | ||
| __CPROVER_ASYNC_1: global=1; | ||
| global=2; |
There was a problem hiding this comment.
// Runs in main thread only ?
| { | ||
| __CPROVER_ASYNC_1: global=1; | ||
| global=2; | ||
| assert(global==2); // to fail |
There was a problem hiding this comment.
// Fails if the spawned thread runs after the main
peterschrammel
approved these changes
Oct 24, 2017
smowton
added a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026 37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table 429c13f Merge pull request diffblue#1520 from smowton/smowton/fix/symbol_table_writer_erase d9f3a2f Revert "Disable OSX builds" 81bb39c Symbol-table writer: fix use of map key after erasure 021fe8f Merge pull request diffblue#1492 from tautschnig/perf-test 0729e3d Merge pull request diffblue#1517 from NathanJPhillips/bugfix/journaling-symbol-table-constructor 93ae9f3 Merge pull request diffblue#1527 from diffblue/revert-1510-always-inline c4ed1ae Revert security-scanner version of recording symbol table e83e307 Fixed scope of moved symbol 535f1df Revert "Fully process always_inline" 0096451 Replace broken copy constructor with move constructor a6adb19 Fix more catch std::string occurances 22a876f Merge pull request diffblue#1523 from reuk/reuk/update-compiling-instructions 8fe258b Update COMPILING with cmake setup instructions 99592b3 Merge pull request diffblue#1504 from andreast271/update-windows-build dff22b8 Make Windows compilation instructions more prescriptive bc3bc8f Merge pull request diffblue#1511 from tautschnig/fix-graphml 358829c Merge pull request diffblue#1510 from tautschnig/always-inline 3e77dd6 Merge pull request diffblue#1496 from smowton/smowton/feature/symbol_table_writer d115b4e catch by const ref instead of by value or non-const ref 444d824 Fix graphml output of concurrency witnesses 08c512d Make Windows compilation instructions more prescriptive bcf8ff3 Update documentation for building cbmc on windows. Update makefiles to use reasonable default compiler for cygwin build. Allow alternative downloader selection from make command line. 728dbb5 Merge pull request diffblue#1508 from smowton/smowton/1420-fragments/value_set_debugging 9d9e50d Merge pull request diffblue#1507 from smowton/smowton/1420-fragments/factor_java_object_init b2104b0 Merge pull request diffblue#1506 from smowton/smowton/1420-fragments/typecheck_expr_cleanup 7175efe Merge pull request diffblue#1505 from smowton/smowton/1420-fragments/invariants 7537302 Adding a java_lang_object_init function 86513ee Merge pull request diffblue#1324 from reuk/reuk/clang-format ea4a777 Merge pull request diffblue#1503 from reuk/reuk/rebuild-ansi-c-when-necessary d9c0598 [pointer-analysis] Better debugging information in pointer analysis 3146336 Remove unnecessary includes in java-typecheck 10b5c8e [java-bytecode/typecheck] Style: Changing assertions in preconditions 2afe377 Fully interpret __attribute__((always_inline)) 8eaf89e Apply symbol replacement in type_arg members 13a7553 Rebuild ansi-c library if non-source dependencies change b97a766 Merge pull request diffblue#1403 from karkhaz/kk-regenerate-arch-flags-binaries a4dc986 Merge pull request diffblue#1484 from diffblue/interpreter_size_t 9d4e0ca Merge pull request diffblue#1217 from KPouliasis/show_functions_dfs c3e6726 Script to automate performance evaluation of CBMC on AWS 912ee38 Improve symbol table style 6b1a49d Add missing goto-statistics file to Makefile d512204 Add cbmc and jbmc as install targets bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019 c5c77ac Merge pull request diffblue#1495 from diffblue/codeowners2 f154d16 Merge pull request diffblue#1487 from martin-cs/goto-analyzer-6-part2 4955417 initialize_goto_model now returns a goto_model 56f924c Merge pull request diffblue#1483 from diffblue/signature_initialize_goto_model eef32db Methods for ai_baset to allow access to the ai_base_domaint for a location. aae984a Disable the regression test for now as it depends on the variable sensitivity domain. 3050c53 Don't stop when recursion found 93f2e1f Use is_bottom() to catch unreachable functions. 5b604ae Update the mock domain with the new ai_domain_baset interface. f9ca353 Add is_bottom() and is_top() to ai_domain_baset and derived domains. 88d8673 Rename the XML output to something a bit more meaningful. 2110cd1 Make formatting stage non-blocking on Travis a24ac3d Fixup compiling.md with more clang-format install instructions c3c24e2 Add symbol table writer 98643d7 initialize_goto_model now returns a goto_model fd6acc5 initial proposal for owners of code f39ae5c use mp_integer for addresses f6ae635 use std::size_t in interpreter 55e6594 Fixup cpplint.py 9d4b827 Update coding standard 8482b35 Add information about using clang-format 1dcc82c Convert COMPILING to markdown format 554cb54 Adjust cpplint to disable whitespace checks by default 6ce0dba Add travis style check f18979a Add clang-format config 622e2e3 Merge branch 'develop' into show_functions_dfs bea696a Regenerated cross-compiled arch flag test binaries 1fab1c1 Fixed show-call-sequences deature of goto instrument; added test suite git-subtree-dir: cbmc git-subtree-split: 739c7f5
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The START_THREAD instruction may induce a number of assignments, which end up as
assignment in the symex_target_equation while the corresponding pc still points
to a START_THREAD instruction. Hence testing assignments must be done
consistently either within the symex_target_equation or within the goto program
level.