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.

Sign up for GitHub

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

Jump to bottom

C Support Changes #581

Merged
merged 11 commits into from
Mar 10, 2017
Merged

C Support Changes #581

merged 11 commits into from
Mar 10, 2017

Conversation

thk123
Copy link
Contributor

@thk123 thk123 commented Mar 2, 2017 •
edited by peterschrammel
Loading

No description provided.

@peterschrammel
Copy link
Member

@thk123, please rebase. This should fix the compilation problem.

@thk123 thk123 force-pushed the feature/c-support-changes branch from 6416334 to a06c295 Compare March 3, 2017 15:37
@thk123 thk123 closed this Mar 3, 2017
@thk123 thk123 force-pushed the feature/c-support-changes branch from c3eac11 to 5a33d91 Compare March 3, 2017 17:50
thk123 added 11 commits March 6, 2017 14:36
Generate stub method for opaque functions
03a4213 
Initial commit making a stub function in the GOTO program for any opaque
functions (i.e. functions for which we don't have a body). This is done
to ensure we can match up the assignments after the opaque function to
the return from the opaque function.
Don't create stub for CPROVER_ functions
06b36cd 
These were having stubs created but they are not opaque functions. This
was because their body gets created after this step.
Create stub argument identifiers for functions with parameters
4b6e9c9 
If opaque functions do not name there parameters, it causes issues later
when we try to call the stub functions. This creates dummy symbols and
names the parameters in the function type.
Pass the whole parameter in when generating the symbol
ddd2cae 
This allows for the symbol builder to inspect other properties of the
type (e.g. is is a this parameter).
Refactored method for generating return symbol name to languaget
b12d2e7 
The name for the return symbol is now generated by languaget. This is so
the name is consistent across different language implementations.
Added a flag for enabling opaque method stubs
13038bf 
As some tests were verifying the functions didn't exist, we need a flag
to turn it on or off. Stubs default to off and are turned on by the flag
--generate-opaque-stubs.

This is an option in CBMC but perhaps it could be applied to other
programs (e.g. applied when compiling C to GOTO).
Use the system_library_symbols when generating stubs
f9bfbbe 
We don't want to generate stubs for any of these symbols as they have
proper internal implementaions that CBMC knows about.
Added comment explaining the type of symbols we aren't stubbing
473dc89
Adding simple regression for struct function
519e08b 
Also made test logs be ignored but git. This test currently fails (correctly) as the integer member of the struct is not being set to the correct value
Use the symbol in expr2c
0e755e6
Call the generate_opqaue_stubs from final
8f68c25 
This doesn't do anything if it is not enabled
@thk123 thk123 reopened this Mar 10, 2017
@peterschrammel peterschrammel merged commit 8dd297e into diffblue:test-gen-support Mar 10, 2017
@thk123 thk123 deleted the feature/c-support-changes branch March 10, 2017 16:47
NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this pull request Aug 22, 2018
@smowton
Squashed 'benchmarks/LIBRARIES/models/' changes from 1e8b77c83..24023…
54a95ff 
…6357

240236357 Merge pull request diffblue#581 from diffblue/forejtv/simpler-file
8ef53a50a simplified constructor for java.io.File
d1c08d982 Put non-simple File.java into simple models
13c22a856 Merge pull request diffblue#578 from diffblue/jeannie/UpdateDTUversion
39202a4e5 Merge pull request diffblue#577 from diffblue/allredj/complete-linked-list-documentation
2d94c7b47 Update deeptest-utils version.
ab300bbe2 Complete documentation of LinkedList
4f77b90dd Merge pull request diffblue#544 from diffblue/collections-reverse
e78b7f02c Tests for Collections model
137622bcf Model for java/util/Collections
422197c51 Added java/util/Collections
33c1410b9 Merge pull request diffblue#576 from diffblue/smowton/admin/increase-to-depth-1600
85000a8ac Bump depth to 1600
927fef36d Merge pull request diffblue#571 from diffblue/zgoriely/linked-list-basic
8621e0d71 Addressing reviewer comments
46376144c Add tests for LinkedList methods
e4782ab96 Implement model for remaining basic LinkedList methods
0a32c4de5 Merge pull request diffblue#566 from diffblue/zgoriely/linked-list
7cc397a82 Add tests for new methods
e86ade7cb Implement methods for LinkedList
6fe84d51a Merge pull request diffblue#569 from diffblue/allredj/update-dtu-131
7bf5a1a80 Update DeepTestUtils to 1.3.1
9df72dd93 Merge pull request diffblue#560 from diffblue/zgoriely/arrays-simple-equals
78228133b Re-enable tests depending on Arrays.equals
b011e0cf5 Add Tests for Simple Arrays.equals
1a76bd166 Implement Simple Model for Arrays.equals
4d14a9a57 Merge pull request diffblue#543 from diffblue/linked-list-add-all
27c9f5da6 Merge pull request diffblue#562 from diffblue/zgoriely/arrays-equals-fix
b19e50c71 Tests for LinkedList init(c)|addAll(c)
394db6890 Modelled java/util/LinkedList.(<init>(Collection)|addAll)
950aae85c Merge pull request diffblue#565 from diffblue/zgoriely/hashset-fix
534a85708 Arrays Equals Model fix - Double and Float
74fa617b8 Fixing HashSet.addAll method
dac4774ce Merge pull request diffblue#542 from diffblue/java-util-optional
396f52c45 Tests for Optional model
d11e8faed Tidying Optional Model
3f8e7e19f Modelled java/util/Optional and java/util/function/(Supplier|Consumer)
8db4ad90e Emptied java/util/Optional and java/util/function/(Supplier|Consumer)
4c3781871 Added java/util/Optional and java/util/function/(Supplier|Consumer)
a6cbe0c51 Merge pull request diffblue#564 from diffblue/zgoriely/arrays-comparator-fix
ab7638920 Fix for Comparator sort test-gen failure
13218fec0 Merge pull request diffblue#545 from diffblue/arrays-sort
bd27eeac1 Fixing up tags in Base64 Models
14f7cda29 Tests for Arrays.sort
8c4c1c524 Model java/util/Arrays.sort
edefabb77 Empty java/util/Comparator
5c39ba9e2 Add java/util/Comparator
941eefa80 Merge pull request diffblue#563 from diffblue/allredj/travis-housekeeping
996c4aab8 Travis: Don't save html report
37640904c Travis: install gauge html-report
72330e6ce Linting
3a97f9fa5 Travis: Remove unneeded addon installs
c6d77308b Merge pull request diffblue#556 from diffblue/allredj/update-modeltests-gitignore
11409e1aa Merge pull request diffblue#375 from diffblue/jeannie/setTimeZoneAndOthers
6b4808330 Update .class files
7deac9024 Tag all failing tests with appropriate ticket no.
c832fba9b Mock Calendar and fix some things in the model
726558344 Re-enable fastTime field in Date model
e5f994525 Updates CProver.nondet methods for not modelled functions.
d43a366cf Updates documentation in javadocs for java.util.Date
e65c0f6aa Tests java.text.SimpleDateFormat
798fd0b5e Models java.text.SimpleDateFormat
0499abc91 Models java.text.DateFormat getTimeZone() and setTimeZone()
6d96405f7 Marks all methods as notModelled() in Format classes
477fcc92d Initial commit for java.text.Format, DateFormat and SimpleDateFormat models.
efd6fe8e3 Tests java.util.GregorianCalendar
e4e0d40ff Tests java.util.Calendar
b87c250f8 Models java.util.GregorianCalendar()
e03f25170 Marks all methods as notModelled() for java.util.GregorianCalendar
ce2549199 Initial commit for java.util.GregorianCalendar
9d85399fa Models java.util.Calendar
d0d31e9ed Marks all methods as notModelled() in java.util.Calendar
71d877078 Initial commit for java.util.Calendar
149aa4da6 Models ZoneInfo getRawOffset() and uses it for getOffset()
8d9a9ac67 Merge pull request diffblue#561 from diffblue/zgoriely/model-test-generator-improvement
0a7e92e0d Fixing a couple bugs in model test generator
7ce6d62a9 Merge pull request diffblue#558 from diffblue/antonia/appendable-annotation
562ffb424 Merge pull request diffblue#559 from diffblue/antonia/enable-TG-3905-tests
e32331aa9 Merge pull request diffblue#555 from diffblue/zgoriely/arrays-fill
4d1111fa6 Enable tests for TG-3905
fb5308932 Move Appendable test to appropriate folder
2149e3ad8 Pick StringBuilder as an Appendable implementation
9b2a4a30a Arrays fill model
1fcddca3f Merge pull request diffblue#557 from diffblue/zgoriely/arrays-equals
0ef93d6dd Updated test class names and test method names
c037628e6 Re-Enabling tests that rely on Arrays.equals
8329b761d Merge pull request diffblue#541 from diffblue/emptier-script
bc31d0bdf Merge pull request diffblue#551 from diffblue/zgoriely/arrays-equals
f9f914b8f Update modelTests .gitignore
8469f6c28 Tests for Arrays.equals methods
2eef3d595 Model for Arrays.equals methods
bf7b6f191 Merge pull request diffblue#550 from diffblue/cesaro/java-sync-fix
1a93b39d5 Re-enable tests in PushbackReader.spec, see e21b471
dd8689737 Merge pull request diffblue#547 from diffblue/svorenova/enable_tests_tg3514
5fd67cde8 Use Gauge tear-down steps
e1b2b5241 Update ticket number for disabled tests for mocking with inheritance
9ee355cd5 Merge pull request diffblue#554 from diffblue/allredj/travis-use-obfuscated-build
5fee9930a Use obfuscated test-gen build in models-library
7502e471d Merge pull request diffblue#540 from diffblue/java-concurrency-synchronization-models
e21b471ab Temporary disabled a number of tests in 'PushbackReader.spec'
7f1eb804d Emptier script
d0b941b83 Changes to support PR cbmc#2280
5915ce44d Merge pull request diffblue#536 from diffblue/antonia/unnecessary-gauge-steps
e8b4888f9 Merge pull request diffblue#538 from diffblue/bugfix/TG-1888/put-tests-in-appropriate-packages
8fd5af6eb Tidy up Verify steps in spec files
da8b4ac38 Don't use java or javax packages
4ec167eec Adding test for checking getPackageFromMethod
91ea20ce3 Put tests in to the package that the function under test is in
6e6b59698 Merge pull request diffblue#533 from diffblue/allredj/testrunner-start-with-unwind-2
57b73a8b0 Merge pull request diffblue#504 from diffblue/forejtv/simple-base64
8907ffd20 Simplified model for Base64
8d521d65d Skip some tests that fail due to TG-3981
35621a7e9 Merge pull request diffblue#530 from diffblue/romain/string-init-charset
efebf5cec Use CProverString.substring
d929a005f Use a reversible version of getBytes
c1e020c3d Add test for constructor from byte[] and charset
07004ec1b Model for String constructor from byte[], charset
136326682 Use equality on name for charsets
e45df98d0 Use CProverString.equals instead of ==
61c713714 Define a CProverString.equals function
c0ef4fe7d Merge pull request diffblue#519 from diffblue/allredj/linkedhashset
338a1cdfc Merge pull request diffblue#528 from diffblue/allredj/simple-linkedhashset
cf1f27e96 Added original model for Base64
8676ea6b5 Merge pull request diffblue#535 from diffblue/antonia/stringreader-optimisations
0f051858c Tests for LinkedHashSet (simple model)
d964fa763 Make HashSet fields package-private (simple model)
beaf7d1bf Simple model for LinkedHashSet
01e2b787c Import LinkedHashSet.java from JDK
400db2ba0 Add missing Diffblue Javadoc tags
f50914877 Use more efficient charAt in StringReader
6a60301b0 Clarify differences from JDK StringReader
c95f30f27 Load a StringReader when loading PushbackReader
8290e5b13 Start generating tests with unwind 2
8861b24f1 Tests for LinkedHashSet
81ca53b05 Model for LinkedHashSet
5d9420c1d Import LinkedHashSet.java from JDK
4e22d539b TestRunner: Factor out debug output
9616e1769 Merge pull request diffblue#531 from diffblue/romain/nondet-initialize-file
8553bf0e5 Activate cproverNondetInitialize for file
c0d1c05dc Merge pull request diffblue#532 from diffblue/allredj/fix-stringbuffer-append
71e3b0788 Merge pull request diffblue#534 from diffblue/allredj/use-fornotmodelled-in-simple-models-2
c0f10640b Merge pull request #529 from diffblue/jeannie/TestRunnerImportsUpdate
65b68beeb Merge pull request diffblue#516 from diffblue/allredj/exhibit-mocking-bug-with-inheritance
2588b96c0 Use appropriate header for tests.
fc3f1c53a Use short name for annotation in TestRunner.
0e9da3a50 Avoid using nondet statements where possible
a20e778b4 Build modelling utils with "package"
753eea477 Copy over cprover package from standard models
67199cdb2 Fix StringBuffer.append
3f2ac3406 Disable tests that suffer from TG-3514
d2dabe327 Make tests sensitive to mocking problems
532d146f3 Merge pull request diffblue#515 from diffblue/antonia/implement-annotation
0048a020c Add tests for classes given in annotations
2e6182b10 Annotate common abstract classes
39f6d72f4 Add java.lang.Appendable interface
bc383f3b2 Add java.io.Flushable interface
83dffab13 Add java.lang.AutoCloseable interface
18bd2e55b Add java.io.Closeable interface
f37ca90df Add java.lang.Readable interface
a8369c332 Add implementation annotation to simple models
d06449814 Show "Preferred..." annotations in Javadoc

git-subtree-dir: benchmarks/LIBRARIES/models
git-subtree-split: 240236357fc9fb1cb87bf5adacaa1b27786ff84b
NathanJPhillips pushed a commit to NathanJPhillips/cbmc that referenced this pull request Sep 6, 2018
Merge pull request diffblue#581 from diffblue/owen-jones-diffblue/use…
23579f4 
…-check-call-when-compiling-tests

Use check_call when compiling tests
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@thk123 @peterschrammel