forked from diffblue/cbmc
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request diffblue#1354 from NathanJPhillips/merge-develop-t…
…o-sss Merge develop to security scanner support
- Loading branch information
Showing
171 changed files
with
3,184 additions
and
1,105 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,34 @@ | ||
static unsigned bar() | ||
{ | ||
unsigned r; | ||
return r; | ||
} | ||
|
||
#ifdef _MSC_VER | ||
|
||
static void foo() | ||
{ | ||
} | ||
|
||
#else | ||
|
||
static void foo() | ||
{ | ||
unsigned len=bar(); | ||
struct { | ||
int a; | ||
union { | ||
int s; | ||
unsigned char b[len]; | ||
} __attribute__ (( packed )) S; | ||
int c; | ||
} __attribute__ (( packed )) *l; | ||
} | ||
|
||
#endif | ||
|
||
int main() | ||
{ | ||
foo(); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
CORE | ||
main.c | ||
|
||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring | ||
^CONVERSION ERROR$ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
extern char src_start[]; | ||
extern char src_end[]; | ||
extern char dst_start[]; | ||
|
||
void *memcpy(void *dest, void *src, unsigned n){ | ||
return (void *)0; | ||
} | ||
|
||
int main(){ | ||
memcpy(dst_start, src_start, (unsigned)src_end - (unsigned)src_start); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
MEMORY { | ||
RAM : ORIGIN = 0x0, LENGTH = 25M | ||
} | ||
|
||
SECTIONS | ||
{ | ||
/* GCC insists on having these */ | ||
.note.gnu.build-id : { } > RAM | ||
.text : { } > RAM | ||
|
||
.src_section : { | ||
src_start = .; | ||
*(.text*) | ||
src_end = .; | ||
} > RAM | ||
|
||
.dst_section : { | ||
dst_start = .; | ||
*(.text*) | ||
dst_end = .; | ||
} > RAM | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
CORE | ||
main.c | ||
-o out.gb -T script.ld -nostdlib | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring | ||
^CONVERSION ERROR$ | ||
-- | ||
Tesing the functionality of goto-cc's linker script parsing | ||
functionality, ensuring that it can get the values of symbols that are | ||
defined in linker scripts. | ||
|
||
This test ensures that goto-cc and ls-parse can: | ||
|
||
- get the value of a symbol whose value indicates the start of a section; | ||
- get the value of a symbol whose value indicates the end of a section. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
extern char src_start[]; | ||
extern char src_size[]; | ||
extern char dst_start[]; | ||
|
||
void *memcpy(void *dest, void *src, unsigned n){ | ||
return (void *)0; | ||
} | ||
|
||
int main(){ | ||
memcpy(dst_start, src_start, (unsigned)src_size); | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
|
||
MEMORY { | ||
RAM : ORIGIN = 0x0, LENGTH = 25M | ||
} | ||
|
||
SECTIONS | ||
{ | ||
/* GCC insists on having these */ | ||
.note.gnu.build-id : { } > RAM | ||
.text : { } > RAM | ||
|
||
.src_section : { | ||
src_start = .; | ||
*(.text*) | ||
src_end = .; | ||
} > RAM | ||
|
||
src_size = src_end - src_start; | ||
|
||
.dst_section : { | ||
dst_start = .; | ||
*(.text*) | ||
dst_end = .; | ||
} > RAM | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
CORE | ||
main.c | ||
-o out.gb -T script.ld -nostdlib | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring | ||
^CONVERSION ERROR$ | ||
-- | ||
Tesing the functionality of goto-cc's linker script parsing | ||
functionality, ensuring that it can get the values of symbols that are | ||
defined in linker scripts. | ||
|
||
This test ensures that goto-cc and ls-parse can: | ||
|
||
- get the value of a symbol whose value indicates the start of a section; | ||
- get the value of a symbol whose value indicates the size of a section, | ||
and whose value has been generated through a basic arithmetic | ||
expression in the linker script. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
extern char sym[]; | ||
|
||
int main(){ | ||
int foo = (int)sym; | ||
return 0; | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
MEMORY { | ||
RAM : ORIGIN = 0x0, LENGTH = 25M | ||
} | ||
|
||
SECTIONS | ||
{ | ||
/* GCC insists on having these */ | ||
.note.gnu.build-id : { } > RAM | ||
.text : { } > RAM | ||
|
||
.src_section : { | ||
sym = .; | ||
*(.text*) | ||
} > RAM | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
CORE | ||
main.c | ||
-o out.gb -T script.ld -nostdlib | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
-- | ||
^warning: ignoring | ||
^CONVERSION ERROR$ | ||
-- | ||
Tesing the functionality of goto-cc's linker script parsing | ||
functionality, ensuring that it can get the values of symbols that are | ||
defined in linker scripts. | ||
|
||
This test ensures that goto-cc and ls-parse can get the value of a | ||
symbol whose value indicates the start of a section. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,4 +1,3 @@ | ||
#include <assert.h> | ||
#include <stdio.h> | ||
|
||
int main() | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,5 +1,3 @@ | ||
#include <assert.h> | ||
|
||
int myfunc(int x, int y) | ||
{ | ||
int z = x + y; | ||
|
Oops, something went wrong.