Commit Graph

3903 Commits

Author SHA1 Message Date
kroening 3818f699db it's gcc_computed_goto
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4033 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:37:26 +00:00
kroening 4eca0d051f computed goto got an ID
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4032 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:35:33 +00:00
kroening ec1463e19a fix for packed and alignment
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4031 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:24:15 +00:00
kroening e6136eaaf5 fix for enum values
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4030 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:24:06 +00:00
kroening 3663e5dfbc further fix static assertions
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4029 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:15:43 +00:00
kroening 390d83e84a fix static assertions
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4028 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:13:23 +00:00
kroening 19e9d95b0e do objective-C block pointers
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4027 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:09:22 +00:00
kroening e8885ef963 second fix for function return types
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4026 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 15:01:06 +00:00
kroening 9dd56d387e fix for function return types
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4025 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 14:56:24 +00:00
kroening 8c81d55e92 fix for static assertions
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4024 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 14:46:49 +00:00
kroening b834da5fe5 properly do zero-width bit-fields
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4023 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 14:17:11 +00:00
kroening e712c7ddee use an example that wors with Visual Studio
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4022 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 13:46:30 +00:00
kroening 7faa9fb124 recursive structs
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4021 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 13:39:22 +00:00
kroening 2e2c52d62d zero-width bit-field
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4020 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 13:37:43 +00:00
kroening 9a528e2820 comment
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4019 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 13:35:43 +00:00
kroening 5228f8ac4c comment
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4018 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 13:31:54 +00:00
kroening da876ee551 deal with anon union/structs
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4016 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 08:49:00 +00:00
kroening be2675fa76 members don't go into scope
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4015 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 08:40:33 +00:00
kroening 23c6b8cfd9 elaborated error message
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4014 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 08:40:11 +00:00
kroening 4a504f90d8 fix for type attributes of parameters
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4013 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-14 08:24:19 +00:00
kroening 5583704598 form
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4012 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 21:34:12 +00:00
kroening 6e75b31bd2 clean
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4011 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 21:33:46 +00:00
kroening 5e4b9c2382 fixes for boolector
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4010 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 20:48:53 +00:00
kroening 6da127ee77 new version of boolector
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4009 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 20:47:48 +00:00
kroening 67c0a2bdd8 pass down solver
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4008 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 20:47:40 +00:00
kroening 93fa2c9d9e CVC and Boolector now allow SMT2
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4007 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 20:47:04 +00:00
kroening 349e15362c fix for compound symbols
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4006 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 16:44:36 +00:00
kroening cbdc42fbc3 fix abstract declarators
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4005 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 16:06:21 +00:00
kroening a959504957 fix bit fields
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4004 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 15:55:14 +00:00
kroening cfbbbe16b3 fix for member declarations
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4003 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 15:44:23 +00:00
kroening 05a0837260 fix for local declartions
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4002 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 15:26:46 +00:00
kroening 97a6bc6f88 fix for enums
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4001 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 11:04:42 +00:00
kroening 9318a8dde7 Regression test witnessing empty (non-nil) locations
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@4000 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 10:04:12 +00:00
kroening b24bc994cf Use appropriate namespace when printing information
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3999 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 09:53:02 +00:00
kroening e51519ade9 Cleanup of linker error/warning reports
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3998 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 09:52:13 +00:00
kroening b77964f777 vectors
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3997 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 09:46:53 +00:00
kroening da4ce0e1aa use already_typechecked trick
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3996 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 09:46:46 +00:00
kroening d22882265c use already_typechecked trick
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3995 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 09:46:25 +00:00
kroening 50b07b15bf replaced the "regents"
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3994 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-13 09:35:08 +00:00
kroening 22d9167317 vector error message
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3993 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:27:05 +00:00
kroening 5244055930 add internal addtions back in
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3992 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:25:33 +00:00
kroening 13a2977212 fix locations
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3991 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:24:37 +00:00
kroening 2f539a3288 fix for globals
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3990 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:21:10 +00:00
kroening 96172a256c fix typedefs
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3989 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:15:31 +00:00
kroening 571a53d00c fix
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3988 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:05:07 +00:00
kroening b1631a5485 fix
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3987 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 21:00:37 +00:00
kroening 6207925745 moved typecheck_declaration()
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3986 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 20:58:10 +00:00
kroening 8973019c1b declaration statements
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3985 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 20:36:53 +00:00
kroening fc2ada34f9 moved typecheck_declaration()
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3984 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 20:36:36 +00:00
kroening 9fc6332287 tag cleanup
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3983 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
2014-06-12 20:34:45 +00:00