replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Fix C enum JSON output 

The subtype must be used.
This commit is contained in:
Peter Schrammel 2019-02-17 11:23:03 +00:00
parent 79ea945b15
commit d8b34f25c8
3 changed files with 39 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
regression/cbmc/enum-trace1/main.c Normal file
View File

@ -0,0 +1,23 @@
#include <assert.h>
enum ENUM
{
E1,
E2,
E3
};
typedef enum ENUMT
{
T1,
T2,
T3
} enum_t;
void test(enum ENUM e, enum_t t)
{
enum ENUM ee = e;
enum_t tt = t;
assert(ee != tt);
}

11
regression/cbmc/enum-trace1/test_json.desc Normal file
View File

@ -0,0 +1,11 @@
CORE
main.c
--json-ui --function test --trace
activate-multi-line-match
EXIT=10
SIGNAL=0
VERIFICATION FAILED
\{\n\s*"hidden": false,\n\s*"inputID": "e",\n\s*"internal": true,\n\s*"mode": "C",\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"stepType": "input",\n\s*"thread": 0,\n\s*"values": \[\n\s*\{\n\s*"binary": "000000000000000000000000000000(0|1){2}",\n\s*"data": ".*E(1|2|3)",\n\s*"name": "integer",\n\s*"type": "enum",\n\s*"width": 32\n\s*\}\n\s*\]\n\s*\},
\{\n\s*"hidden": false,\n\s*"inputID": "t",\n\s*"internal": true,\n\s*"mode": "C",\n\s*"sourceLocation": \{(\n.*)*\},\n\s*"stepType": "input",\n\s*"thread": 0,\n\s*"values": \[\n\s*\{\n\s*"binary": "000000000000000000000000000000(0|1){2}",\n\s*"data": ".*T(1|2|3)",\n\s*"name": "integer",\n\s*"type": "enum",\n\s*"width": 32\n\s*\}\n\s*\]\n\s*\},
--
^warning: ignoring

6
src/goto-programs/json_expr.cpp
View File

@ -206,7 +206,11 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
static std::string binary(const constant_exprt &src)
{
const auto width = to_bitvector_type(src.type()).get_width();
std::size_t width;
if(src.type().id() == ID_c_enum)
width = to_bitvector_type(to_c_enum_type(src.type()).subtype()).get_width();
else
width = to_bitvector_type(src.type()).get_width();
const auto int_val = bvrep2integer(src.get_value(), width, false);
return integer2binary(int_val, width);
}