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

kcc and gcc disagree on well-defined program (packed offsetof) #255

Closed
grosu opened this issue Aug 6, 2016 · 5 comments
Closed

kcc and gcc disagree on well-defined program (packed offsetof) #255

grosu opened this issue Aug 6, 2016 · 5 comments

Comments

@grosu
Copy link
Member

grosu commented Aug 6, 2016

The following program is well-defined according to kcc, yet they show different outputs.

$ gcc 3-array-in-struct.c
$ ./a.out ; echo $?
offsetof: 31
5
$ kcc 3-array-in-struct.c
$ ./a.out ; echo $?
offsetof: 32
5
$ 

Here is the program:

#include <stddef.h>
#include <stdio.h>

struct foo {
  char buffer[31];
  int secret __attribute__ ((packed));
};

int idx = 0;

void setIdx() {
  idx = 31;
}

int main() {
  setIdx();
  struct foo x = {0};
  printf("offsetof: %lu\n", offsetof(struct foo, secret));;
  x.secret = 5;
  char* d = (char*)(&x);
  d += offsetof(struct foo, secret);
  int * e = (int *)d;
  return *e;
}

@diekmann thinks: I specified the struct with the attribute packed, so the offset must be 31. kcc reports undefined behavior if I remove the offsetof and replace it with 31.

@diekmann
Copy link
Contributor

diekmann commented Aug 6, 2016

By the way, in the example code above, setIdx and idx can be ignored (sorry for not cleaning up the example completely).

The gcc documentation says:

packed
The packed attribute specifies that a variable or structure field should have the smallest possible alignment—one byte for a variable, and one bit for a field, unless you specify a larger value with the aligned attribute.
Here is a structure in which the field x is packed, so that it immediately follows a:

          struct foo
          {
            char a;
            int x[2] __attribute__ ((packed));
          };

If we change char buffer[31]; to char buffer[127];, without the __attribute__ ((packed)), we can see that gcc (4.8.4-2ubuntu1~14.04.3) with optimizations is also aligning everything to the 128 byte boundary. Adding __attribute__ ((packed)) to the variable will force it to 127 again.

I did not test what happens if I pack the complete struct, i.e.:

struct foo {
  char buffer[127];
  int secret;
}  __attribute__ ((packed));

Does kcc support this?
This would be important for almost any implementation of binary network protocols.

@chathhorn
Copy link
Member

Yeah, all __attribute__s are currently ignored, but support for packed structs is definitely something we should add.

@ellisonch
Copy link
Contributor

To be clear, "packed" is an extension and is not part of the C standard
(it's not even mentioned), which is why it wasn't originally included. It
is a very commonly used extension, so it would be neat to formalize it for
different implementations.

On Sat, Aug 6, 2016 at 8:44 PM, Chris Hathhorn notifications@github.com
wrote:

Yeah, all __attribute__s are currently ignored, but support for packed
structs is definitely something we should add.


You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#255 (comment),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ABOcp620ZknX4fqB8z_ZTb5BByGaSC4zks5qdSpTgaJpZM4JeRIq
.

@diekmann
Copy link
Contributor

diekmann commented Aug 7, 2016

At least it shouldn't be silently ignored?

@chathhorn
Copy link
Member

Added support in b3b1c78

rv-jenkins pushed a commit that referenced this issue Oct 14, 2016
* Fixed a bug.

* absolute path for csv output file

* Added tests

* Added right tests in the right place.

* Fixed small unimportant bug.
rv-jenkins pushed a commit that referenced this issue Feb 28, 2017
* Squashed 'c-semantics/' changes from f8e7068..27a9e55

27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: 27a9e55

* Squashed 'c-semantics/' changes from 27a9e55..b828da9

b828da9 name not found ==> ill-formed
f273a3b name not found ==> ill-formed

git-subtree-dir: c-semantics
git-subtree-split: b828da9
rv-jenkins pushed a commit that referenced this issue Mar 1, 2017
* Squashed 'c-semantics/' changes from f8e7068..d989a4f

d989a4f Merge #265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: d989a4f

* Squashed 'c-semantics/' changes from d989a4f..1c0d683

1c0d683 Update sizeof-is-prval.C
96afbe0 Value category for sizeof()

git-subtree-dir: c-semantics
git-subtree-split: 1c0d683
rv-jenkins pushed a commit that referenced this issue Mar 15, 2017
* Squashed 'c-semantics/' changes from f8e7068..d9c338b

d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix #269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge #266 (#387)
d989a4f Merge #265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: d9c338b

* Squashed 'c-semantics/' changes from d9c338b..d526c53

d526c53 Merge remote-tracking branch 'c-semantics/master' into tusil1
009c3dc Compile-time evaluation of !true, !false.

git-subtree-dir: c-semantics
git-subtree-split: d526c53819f9d3fa4cfc920bc9629567700a2912

* Squashed 'c-semantics/' changes from d9c338b..cf08f51

cf08f51 Merge remote-tracking branch 'c-semantics/master' into HEAD
1125a70 Result type of relational operators should be bool.

git-subtree-dir: c-semantics
git-subtree-split: cf08f519064700ce8f111084875c77bf386d3259
rv-jenkins pushed a commit that referenced this issue Mar 25, 2017
* Squashed 'c-semantics/' changes from f8e7068..46628b2

46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix #269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge #266 (#387)
d989a4f Merge #265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: 46628b2

* Squashed 'c-semantics/' changes from 46628b2..8b1ddf2

8b1ddf2 Merge remote-tracking branch 'c-semantics/master' into HEAD
0e30e73 Minor fix
2ff8bc8 Forgotten rule
99d1031 Remove ite
adb2fca Fixes
4af078c Enums: various fixes
f68697d UNSPEC
ffbcca9 getAsocNs for enum
1e2724e Enumerator lookup.
cc93394 Check value of enumerators with fixed underlying type.
135aeff Enumerators
ee6cbfd Enums: conversions and promotions
9052eff Enums.

git-subtree-dir: c-semantics
git-subtree-split: 8b1ddf2db4d83c8e91317df5bb60606562ab2931
rv-jenkins pushed a commit that referenced this issue Apr 11, 2017
* Squashed 'c-semantics/' changes from f8e7068..91161bd

91161bd implement destructors and destruction of automatic variables and data… (#417)
d2f2c35 some performance optimizations to kompile (#416)
8c2641b miscellaneous fixes for Boeing demo (#409)
095c475 fix build failure of open source makefile (#414)
794f017 Enums + Enumerators (#413)
46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix #269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge #266 (#387)
d989a4f Merge #265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: 91161bd

* Squashed 'c-semantics/' changes from 91161bd..ea0aeb2

ea0aeb2 Enums were treated as their underlying type while reading.

git-subtree-dir: c-semantics
git-subtree-split: ea0aeb2
rv-jenkins pushed a commit that referenced this issue Apr 18, 2017
* Squashed 'c-semantics/' changes from f8e7068..e887f49

e887f49 fix issue with argv having type qualifiers causing stuck configuration (#427)
8c03f14 Computed Types and Categories for Def Args (#421)
88c186b Default arguments (#408)
632f0a6 Issue with enum read (#419)
ca3cec0 Fixes for Toyota ITC benchmark regressions. (#420)
91161bd implement destructors and destruction of automatic variables and data… (#417)
d2f2c35 some performance optimizations to kompile (#416)
8c2641b miscellaneous fixes for Boeing demo (#409)
095c475 fix build failure of open source makefile (#414)
794f017 Enums + Enumerators (#413)
46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix #269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge #266 (#387)
d989a4f Merge #265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: e887f49

* Squashed 'c-semantics/' changes from e887f49..baad6da

baad6da Merge remote-tracking branch 'c-semantics/master' into HEAD
c345905 missing cfg:alignofReference

git-subtree-dir: c-semantics
git-subtree-split: baad6daa7ae30f4a50e437a6903e6d5bcf271121
rv-jenkins pushed a commit that referenced this issue Apr 19, 2017
* Squashed 'c-semantics/' changes from f8e7068..e887f49

e887f49 fix issue with argv having type qualifiers causing stuck configuration (#427)
8c03f14 Computed Types and Categories for Def Args (#421)
88c186b Default arguments (#408)
632f0a6 Issue with enum read (#419)
ca3cec0 Fixes for Toyota ITC benchmark regressions. (#420)
91161bd implement destructors and destruction of automatic variables and data… (#417)
d2f2c35 some performance optimizations to kompile (#416)
8c2641b miscellaneous fixes for Boeing demo (#409)
095c475 fix build failure of open source makefile (#414)
794f017 Enums + Enumerators (#413)
46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix #269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge #266 (#387)
d989a4f Merge #265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes #264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: e887f49

* Squashed 'c-semantics/' changes from e887f49..4040b08

4040b08 Lookup for unscoped enumerators in class.
619042c Opaque enums
41bd465 Enums in functions
51b1a12 enumerators: one more test case

git-subtree-dir: c-semantics
git-subtree-split: 4040b08

* Update name.k

* fix non confluent rules
rv-jenkins pushed a commit that referenced this issue Sep 27, 2017
* Fixes #321. (#322)

* Removed cyclic isKItem rules. (#323)

* Removed cyclic isKItem rules.

* Removing declaration, too

* Basic Field declaration and member pointers initialization (#311)

* ptrmem3.C passing

* Addressing some comments

* Derived joinPointerBytes

* Fixed setting for limited x86 profile.

* Another fix

* Added convertType default. trmem3.C works

* Extracted common functionality.

* Fixing syntax

* Class name lookup

* Field declaration.

* Member pointers initialization.

* Addressing review comments.

* Removed commented out code.

* addressing comments

* Reimplemented <=QualSig

* delete unused profiles and create a second profile which reverses evaluation order (#317)

What this does is create a flag to kompile which reverses the order of rules prior to
compilation to OCAML. We also delete the 78k0r and x86-gcc-limited-libc profiles from
the installer since they aren't very good and aren't being used to my knowledge.
We then create a second profile which uses this flag. As a result, by using both profiles
you get much higher probability of detecting undefined behavior and test failures which arise
from extremely simple nondeterminism in your program.

* Small fix (#324)

* Relax type required by %s format specifier.

* Clean up, check %s format spec length.

* Test for %s relaxed type requirement.

* support -iquote flag (#325)

* some minor fixes to kcc script to work with project provided by DENSO (#328)

* some minor fixes to kcc script to work with project provided by DENSO

* add build number to distributable

* Some v*printf functions, UB for uninit va_list. (#329)

* Some v*printf functions, UB for uninit va_list.

* CERT citation.

* Updated expected output.

* longjmp with nonexistent env UB. (#330)

* longjmp with nonexistent env UB.

* CERT citation.

* Updated expected error output.

* Empty brace-init for empty aggregate class. (#332)

* Empty brace-init for empty aggregate class.

* Incorporated comments.

* Relaxed condition of compoundInit

* Working with a field.

* Limited brace-or-equal-initializers.

* Fixed issues pointed out in the review

* new error infrastructure (#333)

* new error infrastructure

* fail compile test alterations for x86_64 profile

* fail test alterations for x86_64 profile

* error codes alterations for new error infrastructure

* update script to build opam dependencies

* fix missing path entry

* fix unit-fail-compilation tests by adding -Werror

* add csv renderer

* improve performance with nailgun and fix a few bugs

* make eclipse plugin work again

* fix typo in -Wno-unspecified and add tests

* add documentation for rv-error

* fix ignored flag (#341)

* compute path to rv-error in kcc script (#352)

* compute path to rv-error in kcc script

* temp debugging output to figure oiut what is going on in jenkins build

* Revert "temp debugging output to figure oiut what is going on in jenkins build"

This reverts commit c3f330b611b07505311dc804ab2a001e780c3528.

* fix trailing newline in stdout for command -v

* fix issue with incompatibility between java and ocaml json

* Add framework for message output from kcc (#353)

* Add framework for message output from kcc

With rv-licenseing 1.3, a license can carry a message.
This changes make kcc print that message by default when used with -c
or to link a program (with options to turn it off if it interferes
with a build).

* Use existing tempFile function in kcc script

* Need a tab for option to actually be parsed (#357)

* support for ifdef and file glob suppression in rv-error (#337)

* support for ifdef and file glob suppression in rv-error

* fix absolute path

* optimization for duplicates + fix for makefile

* fix c++ parser to emit both absolute and relative path

* use more portable idiom for getting absolute path in bash

* fix bug when preprocessing fails

* update documentation

* add rv-error bin to path of rv-error jar

* fix exit code 255 and improper failure to error when no files specified (#362)

* add line to make clean that was missing (#366)

* improve performance of memory access (#349)

* improve performance of memory access

* fix whitespace

* fix check that was actually necessary but I removed

* Name lookup (#339)

* Reimplemented brace initialization.

* Evolving pointer to memeber and functional casts.

* static members

* Static data members work (no class initializer).

* Static data member definition and lookup.

* Reworked name lookup

* Resolution for class statics

* Towards translating brace-or-init initializers

* Towards a standard-based name lookup

* Advanced brace-or-equal-initialization

* Fix narrowing type condition.

* Fixed Statics

* Fixed some failing tests

* Progress on failing tests.

* Fixed function lookup

* Fixed static member lookup

* Refactorings

* Addressing review

* Proper Qualified Name Lookup

* Added Name lookup example

* Small refactorings.

* Fixed namespace lookup and declaration

* Fixes

* Fixed namespace qualified name lookup

* Reusing existing constructs for static declarations

* Addressed xvalue comment.

* print types involved in effective type computation (#364)

* print types involved in effective type computation

* fix comments and remove unused function

* update test outputs

* fix issue with incorrect preprocessor used for c++ (#370)

* fix issue with incorrect preprocessor used for c++

* fix more issues with $isCPP

* Semantics for some stdio functions. (#334)

* Semantics for some stdio functions.

* Opaque stdlib values, refactored joinBytes.

* Refactor bit:: to function.

* Fixes.

* fputs, fixes.

* Float formatting not working.

* Rearranged builtins handling.

* Fixes.

* Stdio file positioning functions; fixes.

* fflush, freopen, vfprintf, tmpfile, set*buf.

* fread, fgets, fwrite, ungetc.

* Fixes, scanf stub.

* *scanf.

* Better buffering.

* Fixes.

* Fixes.

* Some stdio tests from glibc.

* Fixes.

* Fixes.

* Couple more tests.

* Fixes.

* miscellaneous fixes to C++ in preparation for work on exceptions (#375)

* miscellaneous fixes to C++ in preparation for work on exceptions

includes:
  * fix for parser issue where typedef of an anonymous class
    was parsed incorrectly
  * implement alignof
  * fix a number of issues with c style casts
  * translation-time semantics of exceptions
  * fix an issue where ill formed initializers were detected too late
  * fix computeSCS
  * miscellaneous fixes for bitwise operators

* bug fixes

* fix exponential parsing time of one particular rule (#377)

* Fix confluence bug. (#378)

* Fixes kframework/c-semantics#264 (#379)

* refactor alignment to be an intrinsic property of objects (#376)

* refactor alignment to be an intrinsic property of objects

* fix eval to use Plugin.get

* Static function members (#369)

* Updated getLinkage for static class members

* Static member function semantics and tests.

* Added tests to the right place.

* Added external definitions for class statics

* Function members seem to work.

* Fixes

* Refactorings

* isBaseClassOf and getInnermostNamespace

* Reworked function types for class members

* This

* Added test.

* Fixed small glitch.

TODO: fix overload resolution for class member functions

* semantics for several features involving tests containing exceptions (#380)

* semantics for several features involving tests containing exceptions

This contains:

* some minor refactoring of how alignment of objects is computed
* code to deal with bitwise and on an aligned pointer and an integer
* support for comma expressions
* support for throwing exceptions and catching them with catch(...)
* added some tests covering these features to the test suite

* fix configuration structure mismatch in ocaml

* fix some test failures

* fix broken build

* add inRange for SymLoc

* catching exceptions of a particular type and rethrowing exceptions (#382)

* catching exceptions of a particular type and rethrowing exceptions

includes the following code:

* catching exceptions of a particular type
* rethrowing the current exception
* some more operations on floats
* exception specifications
* some fixes to conditional operators
* a minor fix to the ocaml backend involving #as patterns

* add tests

* remove test that gcc does not pass

* fix es: to exceptions:

* Merge kframework/c-semantics#265 (#384)

* Squashed 'c-semantics/' changes from f8e7068..27a9e55

27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes kframework/c-semantics#264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: 27a9e55fcbc5c9ef4a3271a4f4aab7a9fd19d989

* Squashed 'c-semantics/' changes from 27a9e55..b828da9

b828da9 name not found ==> ill-formed
f273a3b name not found ==> ill-formed

git-subtree-dir: c-semantics
git-subtree-split: b828da994a68fee6899ac2c764ec10fab5e0abbe

* Merge kframework/c-semantics#266 (#387)

* Squashed 'c-semantics/' changes from f8e7068..d989a4f

d989a4f Merge kframework/c-semantics#265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes kframework/c-semantics#264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: d989a4faf9385514903fb2c4d3dac1e8fed2886a

* Squashed 'c-semantics/' changes from d989a4f..1c0d683

1c0d683 Update sizeof-is-prval.C
96afbe0 Value category for sizeof()

git-subtree-dir: c-semantics
git-subtree-split: 1c0d683a38c25e3a4853e79a4b6a1b2a86d7a21c

* Method overloading (#386)

* Refactored method overload and call semantics

* Small fix

* Addressed review comments.

* Refactored candidate sets (#388)

* Some stdio UB checks. (#385)

* Some stdio UB checks.

* CSV entries.

* Fix.

* CERT citation, error codes.

* Require os-settings.k

* Imports INT.

* Update OcamlBackend.java

* fix kframework/c-semantics#269 (#390)

* various fixes involving classes (#389)

includes:

* improvements to c++ parser, including a fix for anonymous unions
* fixes to guard isBaseClassOf against the case where B and D are the same type
* support for arrow operator
* support for more arithmetic operations involving floats
* while loops
* track whether initialization is copy-init or direct-init
* fix brace-or-equal-initializer for classes
* break statement for loops
* fix a bug where static storage objects with no initializer weren't being default initialized
* refactor initialization code
* more support for reinterpret casts
* support for --x
* getAssociatedClasses for complete class types

* Add setting to allow  __restrict and __restrict__ variants

This resolves the issue #345 that our previous
implementation by #define __restrict restrict
breaks with autoconf detection of restrict support, which
tests first whether __restrict works, and if it does will
emit #define restrict __restrict.

With this commit the lexer recognizes __restrict and __restrict__
as a new "RestrictReserved" token, which the translation semantics
either canonicalizes to the plain Restrict or signals as an error,
following the new Bool ::= cfg:reservedKeywordAllowed(String) setting.

All current profiles are based on gcc which allows these variant keywords,
so the error reporting code is not tested!

* Use existing SE label for error reporting

* Remove SE-TCANON2 bad examples until we can trigger it

* Fix typo in open-source profile.

* Unions (#396)

* List initialization for unions.

* initialization from brace-or-equal-initializer

* Progress towards anonymous unions

* Fixed unnamed structs

* create anonymous function applications in K (#392)

* create #with expression for functional update of record-like KApply on RHS

* update to new syntax and add functions that don't preserve sort

* exclude unnecessary cases for performance reasons

* change syntax once again to be closer to function application

* fix #fun in side condition

* fix name of function

* add comment per traian's request

* overloading operators + default constructor + misc fixes (#397)

* overloading operators + default constructor + misc fixes

includes:

* a fix to suppress a very large warning from the ocaml compiler
* fixes to clang-kast to support constructors better
* a fix to the ocaml backend to allow functions that reflect the configuration
  to access thread-local state
* move parameter binding to execution semantics only
* memory read of values of class type
* implicitly defaulted constructor declaration and definition
* remove storage duration from figureInit because constructors don't know
  what duration of object they're constructing when they invoke figureInit
* refactor this for member functions
* default initialization of classes and arrays of classes
* add operator overloading for operator&, operator->, and operator,.

* fix build errors + add json fix for runner script

* fix broken unit test

* Revert "overloading operators + default constructor + misc fixes (#397)"

This reverts commit 1e217ab13c120e51fb6c08064593e16c3a389ba6.

* Revert "Revert "overloading operators + default constructor + misc fi… (#400)

* Revert "Revert "overloading operators + default constructor + misc fixes (#397)""

This reverts commit 07ff5f2be4b0d1b014b98f281e84df3d1583a36a.

* fix non confluent rules

* Restrict refactoring. (#358)

* Move restrict check from ptr deref to read/write.

* Better restrict check.

* Minor optimizations to the restrict check.

* Update function-call.k

* Enumprep2 (#401)

* Squashed 'c-semantics/' changes from f8e7068..d9c338b

d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix kframework/c-semantics#269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge kframework/c-semantics#266 (#387)
d989a4f Merge kframework/c-semantics#265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes kframework/c-semantics#264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: d9c338b9b44222f302f2e9636badc434884db111

* Squashed 'c-semantics/' changes from d9c338b..d526c53

d526c53 Merge remote-tracking branch 'c-semantics/master' into tusil1
009c3dc Compile-time evaluation of !true, !false.

git-subtree-dir: c-semantics
git-subtree-split: d526c53819f9d3fa4cfc920bc9629567700a2912

* Squashed 'c-semantics/' changes from d9c338b..cf08f51

cf08f51 Merge remote-tracking branch 'c-semantics/master' into HEAD
1125a70 Result type of relational operators should be bool.

git-subtree-dir: c-semantics
git-subtree-split: cf08f519064700ce8f111084875c77bf386d3259

* add rudimentary error reporting back to open source semantics (#403)

* add rudimentary error reporting back to open source semantics

* fix build error

* Unions 2 (#405)

* Namespace unions seem to work.

* Refactorings

* Anonymous union through DeclaratorAndSpecifiers

* various minor fixes for classes (#406)

includes:

* fix an enormous ocaml warning
* add explicit keyword and default keyword to parser
* add a fix to properrly detect value initialization in parser
* fail the kompile build if we have warnings
* fix alignment and size of class types
* fix a minor confluence error in conversion.k
* add semantics for this keyword in expressions to translation semantics
* add some types to support for extern "C"
* support calling 2-arg main function
* fixes for constructors
* value initialization of classes and arrays
* direct initialization and copy initialization from derived class of class type objects
* refactoring of new code to support class types better
* fix broken overloading cases involving resolveEmptyOverload
* substantial improvement to implicit conversion sequences for overloading
* return statement with no operand
* fix broken code for overloading for arguments which are BraceInit
* support computing value category of overloaded operators
* add sqrt function to ocaml backend

* More restrict check tweaks. (#404)

* Restrict check tweaks.

* Move some overhead to block exit.

* Base glob. restricts on fileScope instead of main.

* Fix.

* Minor fix.

* C++ enterRestrictTU.

* Small patch for #fun compilation (#407)

* Enums + Enumerators (#413)

* Squashed 'c-semantics/' changes from f8e7068..46628b2

46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix kframework/c-semantics#269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge kframework/c-semantics#266 (#387)
d989a4f Merge kframework/c-semantics#265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes kframework/c-semantics#264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for non-standard bitfield types.
d7d9c5e Refactoring of qualified types.
0be621f more fixes for constraint violation error recovery
8d824ef recover from  nonfatal constraint violations
3a5b0ab Merge pull request #130 from dwightguth/shared
157f341 fix bug in makefile resulting from renamed flag
18772c3 Merge branch 'master' into shared
b3a6c0f add ignored flags for libjpg
414af52 try another fix for race
84a64c0 undo test of c semantics licensing changes
65ae77e change c semantics license
aed9cc1 fix non confluent incorrect behavior bug
da0b63f fix flag
0ce9500 minor performance optimizations
073f236 c semantics improvements for threads

git-subtree-dir: c-semantics
git-subtree-split: 46628b282e3cd70d67906d41c565ce3393668de2

* Squashed 'c-semantics/' changes from 46628b2..8b1ddf2

8b1ddf2 Merge remote-tracking branch 'c-semantics/master' into HEAD
0e30e73 Minor fix
2ff8bc8 Forgotten rule
99d1031 Remove ite
adb2fca Fixes
4af078c Enums: various fixes
f68697d UNSPEC
ffbcca9 getAsocNs for enum
1e2724e Enumerator lookup.
cc93394 Check value of enumerators with fixed underlying type.
135aeff Enumerators
ee6cbfd Enums: conversions and promotions
9052eff Enums.

git-subtree-dir: c-semantics
git-subtree-split: 8b1ddf2db4d83c8e91317df5bb60606562ab2931

* fix build failure of open source makefile (#414)

* miscellaneous fixes for Boeing demo (#409)

* miscellaneous fixes for Boeing demo

includes:
  * k++ wrapper script which includes libstdc++
  * fixes for value category conversions
  * unify QualId between Namespace and Class
  * improved error reporting of types
  * calling std::terminate
  * fixes for implicit object parameter conversion
  * calling via a function pointer
  * fix a bug where asignment expressions were being evaluated at translation
  * incomplete draft of destructor functionality
  * variadic arguments to functions
  * noexcept exception specification
  * a few other very minor fixes to stuck configurations

* fix test failures

* minor test fixes

* fix broken test

* some performance optimizations to kompile (#416)

* implement destructors and destruction of automatic variables and data… (#417)

* implement destructors and destruction of automatic variables and data members

* fix traian's comment

* Fixes for Toyota ITC benchmark regressions. (#420)

* Issue with enum read (#419)

* Squashed 'c-semantics/' changes from f8e7068..91161bd

91161bd implement destructors and destruction of automatic variables and data… (#417)
d2f2c35 some performance optimizations to kompile (#416)
8c2641b miscellaneous fixes for Boeing demo (#409)
095c475 fix build failure of open source makefile (#414)
794f017 Enums + Enumerators (#413)
46628b2 Small patch for #fun compilation (#407)
2ecd8fe More restrict check tweaks. (#404)
c95b335 various minor fixes for classes (#406)
80b1724 Unions 2 (#405)
584fa6f add rudimentary error reporting back to open source semantics (#403)
bd15701 Enumprep2 (#401)
7de6ef2 Restrict refactoring. (#358)
cf8be6e Revert "Revert "overloading operators + default constructor + misc fi… (#400)
d9c338b Revert "overloading operators + default constructor + misc fixes (#397)"
47b91b4 overloading operators + default constructor + misc fixes (#397)
7938568 create anonymous function applications in K (#392)
1b22b35 Unions (#396)
504f59c Fix typo in open-source profile.
54fbb95 Remove SE-TCANON2 bad examples until we can trigger it
665cb0d Use existing SE label for error reporting
0bed52c Add setting to allow  __restrict and __restrict__ variants
7ab4711 various fixes involving classes (#389)
13cbecf fix kframework/c-semantics#269 (#390)
f8e2671 Some stdio UB checks. (#385)
e90c1a6 Refactored candidate sets (#388)
0287dd8 Method overloading (#386)
6430f9a Merge kframework/c-semantics#266 (#387)
d989a4f Merge kframework/c-semantics#265 (#384)
58b4b81 catching exceptions of a particular type and rethrowing exceptions (#382)
27a9e55 semantics for several features involving tests containing exceptions (#380)
aa4cf12 Static function members (#369)
ca863f7 refactor alignment to be an intrinsic property of objects (#376)
fc7c232 Fixes kframework/c-semantics#264 (#379)
6feb47c Fix confluence bug. (#378)
65979a4 fix exponential parsing time of one particular rule (#377)
6cd2af9 miscellaneous fixes to C++ in preparation for work on exceptions (#375)
966b06c Semantics for some stdio functions. (#334)
281841d fix issue with incorrect preprocessor used for c++ (#370)
b7e88d0 print types involved in effective type computation (#364)
6b8b42e Name lookup (#339)
9d0d50e improve performance of memory access (#349)
ab0db81 add line to make clean that was missing (#366)
27dfe57 fix exit code 255 and improper failure to error when no files specified (#362)
32a0e48 support for ifdef and file glob suppression in rv-error (#337)
a650f78 Need a tab for option to actually be parsed (#357)
80b5ae7 Add framework for message output from kcc (#353)
504245d compute path to rv-error in kcc script (#352)
dc6856e fix ignored flag (#341)
e08e398 new error infrastructure (#333)
28f7c49 Empty brace-init for empty aggregate class. (#332)
64edd06 longjmp with nonexistent env UB. (#330)
64efca1 Some v*printf functions, UB for uninit va_list. (#329)
2417196 some minor fixes to kcc script to work with project provided by DENSO (#328)
8fac435 Merge commit '2b470d'
63ab4b8 support -iquote flag (#325)
50cc85f Small fix (#324)
1e33bbc delete unused profiles and create a second profile which reverses evaluation order (#317)
5466d36 Basic Field declaration and member pointers initialization (#311)
f065197 Removed cyclic isKItem rules. (#323)
21530eb Fixes #321. (#322)
946fea4 Merge pull request #258 from diekmann/patch-1
95b4b47 Added build dependencies + ubuntu version
66b31eb c90-style implicit function decls in error recovery (#318)
abf960b fix issues reported by DENSO in examples directory (#316)
e3f02a2 Bitfields (#305)
f8a7db9 polymorphic syntax productions (#298)
d073df2 Several small fixes for code provided by DENSO (#312)
29ada4b Add name field to nonterminals and create record-like productions (#297)
31aa933 update help message based on Grigore's feedback (#309)
31e5ada Update README.md (#307)
3c43577 Ignore files and update license (#304)
f8ecb61 refactor attributes (#296)
75dc4c2 as pattern in K + some cleanup of C++ semantics using new syntax (#294)
229358e fix performance regression relating to locations in linking errors (#290)
da4507f Recording CSV errors at linking, too. (#288)
a13a17c uniform formatCitations with formatError. (#287)
cf569c4 fix flags used by eclipse by default (#286)
60e86f4 Citations (#275)
0ae800d Locations for link errors. (#283)
26d56fa add constraint violation for * operator (#285)
74e863e new + delete + library + error refactoring + overloading (#276)
8f23480 Add distinct char type. (#282)
4c067f7 draft of code in kcc for eclipse plugin (#281)
b7ef412 Fixes #272. (#274)
16dae2d Fixes #264. (#265)
4650b93 dynamic initialization + some undefinedness + location information + address operator (#258)
c47f3b4 Fixes #261. (#262)
4b31752 Reformat errors (#260)
54e2d77 Fixed a bug. (#255)
4b7b33f fix bug reported relating to alignment check in execution semantics for assignment (#259)
8828cb5 refactoring to initializer + significant fixes for cond1-3.C (#252)
505d4ee Added support for different precision floats. (#251)
2444097 Completely removed cil-semantics. (#254)
979e330 Memo k hash2 (#244)
4153b2f auto type + references + increment and decrement + loops + compound a… (#248)
ba22efd fix bug where wrong variable sort was applied as attribute, leading t… (#250)
5795288 Minor cleanup to the kcc script. (#249)
28123d6 assembly files in kcc script + a minor fix for setjmp on glibc (#245)
b2f6a87 array g++ tests (#238)
24c63f1 Disable effective type tracking on native locs. (#241)
3423e4a Init regress (#240)
21dfd23 Comp init (#239)
b3b1c78 Support for gcc packed struct/unions. (#228)
c496f12 fix handling of -L, -l, and -Wl (#235)
c791da9 Using new parameterized hashing function for memoization (#229)
82e121d initial commit of g++.dg test suite (#230)
12f9002 L-CMR1 => L-CMRE1. (#233)
ab05a88 Uninit auto (#232)
ef547ba initial draft of some stuff relating to templates (#227)
da5dd06 interview challenge - code redundancy in k (#226)
7937b32 fix install instructions for c semantics again (#224)
712124e Fixes to setjmp/longjmp. (#223)
c31a945 Some more stdarg.h-related errors. (#221)
9507f11 Little fixes to error messages. (#220)
e21fe6b Offsetof (#222)
b5f622d Improve time spent parsing (#219)
b9ed102  c++ linking and execution semantics for hello world program (#217)
59da089 Nested anon - second try (#216)
36e9ab0 first stab at c++ translation semantics (#214)
a89714b Adding -no-pedantic option to kcc (#215)
9d1e2ce Tracking whether a Cab belongs to a system header. (#212)
37a3b7f refactor out linking semantics from C semantics and combine it into C… (#211)
a4c2b10 C++ preprocessor, parser, kcc script (#210)
4aac020 reorganize code into c and c++ (#209)
59a1487 compute padding offsets faster (#208)
7c55428 use arrays for intra-object data (#205)
c9ead5c Preprocessor warnings (#207)
6042c2e Added a framework for filtering warnings (#204)
274d56a more performance optimizations (#201)
30ff109 fix makeUnknown for struct padding (#198)
06d672d Relax eff type checks on malloc'd regions. (#199)
c94a774 fix constraint violation issue with cerberus test (#197)
6c89ce1 Some fixes to handling of alignment (#194)
ad25935 Reworking strict aliasing enforcement. (#175)
38a1a65 performance improvements (#189)
bb85edb fix bug with block numbers in spin (#188)
18f4d00 Fix for printf modifiers (#185)
18e9c81 more fixes relating to provenance, pointers, and unspecified values (#178)
9db8d8a fix -dM issue reported by customer (#181)
ef18040 No and or prec (#179)
fd02cf7 Fix for external local declarations (#177)
eb8f2e1 Syntax error (#173)
fc1bd59 improvements based on cerberus test suite (#163)
c6d362a module qualify klabels (#159)
5c870e2 fix build (#157)
c2c9170 remove xml-to-k script and inline its functionality into cparser
99efd59 optimizations to completeTagInExtDecl(s)
17c5500 slightly optimize rules that index poorly (#152)
64d66bf interpreter execution mode for compilation (not linking) (#151)
f62c638 fix missing examples and csv entries (#148)
0d4481b Printf field width, some work on precision support (#149)
cc28c58 several fixes for the native plugin and kcc (#147)
70c1622 Couple lint checks
ee85406 Merge branch 'master' into fixes2
fb5ae2b fix test failure on limited profile
4558f66 fix tests
69d3ce0 update test output with new error message format
b00e9c4 Fixes #145.
fd95339 add at_quick_exit
85aa69d more minor fixes for libjpeg, ffmpeg, and sqlite
4bbe6a4 fixes to tests + issue with evaluation order of struct definitions
a163517 add semantics for vsnprintf
4b62138 add atexit to header files
f97ff33 more minor fixes
35597a0 pthread_atfork and atexit
45e0290 minor fixes
96ad2e0 Merge pull request #132 from dwightguth/constraint
c20d5a8 Merge pull request #137 from runtimeverification/bitfields
1b6a4fe Fix issue with typedefs in bitfields.
7033984 fix remaining tests
b3f0cec Merge remote-tracking branch 'upstream/master' into constraint
f8b1499 fix regression in function type compatibility
cd7d3db minor fixes
783081d fix line number
717730a Merge branch 'master' into nullpointer
347c55a Merge branch 'master' into constraint
a6ec96f Bitfield test.
f336279 implementation defined behavior reading bits of a null pointer value
d81889d Merge branch 'master' of https://github.com/runtimeverification/rv-match into unqual
e886c38 Various minor fixes.
bd55304 fix remaining bugs in native test suite
4d259c8 rough draft of native call test suite
fec69fa temp
c97c696 fix case
ef25c77 fix error with side effects in k cell + fix a non confluent test
48ed5c0 Refactor type compatibility + minor fixes.
805113d Split out typeDeclaration from the Type sort.
f522720 Some test fixes.
1c15724 Check for n…
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants