diff --git a/Strata/Backends/CBMC/BoogieToCBMC.lean b/Strata/Backends/CBMC/BoogieToCBMC.lean index 4ca111003..a20ec43d4 100644 --- a/Strata/Backends/CBMC/BoogieToCBMC.lean +++ b/Strata/Backends/CBMC/BoogieToCBMC.lean @@ -41,7 +41,6 @@ def myProc : Boogie.Procedure := match SimpleTestEnvAST.fst.decls.head!.getProc? | .some p => p | .none => panic! "Expected procedure" - class IdentToStr (I : Type) where toStr : I → String @@ -60,23 +59,14 @@ instance : HasLExpr Boogie.Expression BoogieIdent where def exprToJson (I : Type) [IdentToStr I] (e : Lambda.LExpr Lambda.LMonoTy I) (loc: SourceLoc) : Json := match e with | .app (.app (.op op _) left) right => - let leftJson := match left with - | .fvar varName _ => - if IdentToStr.toStr varName == "z" then - mkLvalueSymbol s!"{loc.functionName}::1::z" loc.lineNum loc.functionName - else - mkLvalueSymbol s!"{loc.functionName}::{IdentToStr.toStr varName}" loc.lineNum loc.functionName - | _ => exprToJson (I:=I) left loc - let rightJson := match right with - | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{IdentToStr.toStr varName}" loc.lineNum loc.functionName - | .const value _ => mkConstant value "10" (mkSourceLocation "ex_prog.c" loc.functionName loc.lineNum) - | _ => exprToJson (I:=I) right loc + let leftJson := exprToJson (I:=I) left loc + let rightJson := exprToJson (I:=I) right loc mkBinaryOp (opToStr (IdentToStr.toStr op)) loc.lineNum loc.functionName leftJson rightJson | .const "true" _ => mkConstantTrue (mkSourceLocation "ex_prog.c" loc.functionName "3") | .const n _ => mkConstant n "10" (mkSourceLocation "ex_prog.c" loc.functionName "14") | .fvar name _ => - mkLvalueSymbol s!"{loc.functionName}::{IdentToStr.toStr name}" loc.lineNum loc.functionName + mkLvalueSymbol (getIdent (IdentToStr.toStr name) loc.functionName) loc.lineNum loc.functionName | _ => panic! "Unimplemented" def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json := @@ -90,7 +80,7 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json := ("id", "symbol"), ("namedSub", Json.mkObj [ ("#source_location", mkSourceLocation "ex_prog.c" loc.functionName "5"), - ("identifier", Json.mkObj [("id", s!"{loc.functionName}::1::{name.toPretty}")]), + ("identifier", Json.mkObj [("id", getIdent name.toPretty loc.functionName)]), ("type", mkIntType) ]) ] @@ -101,7 +91,7 @@ def cmdToJson (e : Boogie.Command) (loc: SourceLoc) : Json := let exprLoc : SourceLoc := { functionName := loc.functionName, lineNum := "6" } mkCodeBlock "expression" "6" loc.functionName #[ mkSideEffect "assign" "6" loc.functionName mkIntType #[ - mkLvalueSymbol s!"{loc.functionName}::1::{name.toPretty}" "6" loc.functionName, + mkLvalueSymbol (getIdent name.toPretty loc.functionName) "6" loc.functionName, exprToJson (I:=BoogieIdent) expr exprLoc ] ] @@ -195,6 +185,20 @@ partial def stmtToJson {P : Imperative.PureExpr} (I : Type) [IdentToStr I] [HasL blockToJson (I:=I) elseb loc, ]) ] + | .loop guard _ _ body _ => + let converted_guard : Lambda.LExpr Lambda.LMonoTy I := @HasLExpr.expr_eq P (I:=I) _ ▸ guard + Json.mkObj [ + ("id", "code"), + ("namedSub", Json.mkObj [ + ("#source_location", mkSourceLocation "from_andrew.c" loc.functionName "8"), + ("statement", Json.mkObj [("id", "while")]), + ("type", emptyType) + ]), + ("sub", Json.arr #[ + exprToJson (I:=I) converted_guard loc, + blockToJson (I:=I) body loc + ]) + ] | _ => panic! "Unimplemented" end @@ -368,6 +372,8 @@ def testSymbols (proc: Boogie.Procedure) : String := Id.run do -- Hardcode local variable for now let zSymbol := createLocalSymbol "z" proc.header.name.toPretty + let sumSymbol := createLocalSymbol "sum" proc.header.name.toPretty + let countSymbol := createLocalSymbol "count" proc.header.name.toPretty -- Build symbol map let mut m : Map String CBMCSymbol := Map.empty @@ -377,10 +383,12 @@ def testSymbols (proc: Boogie.Procedure) : String := Id.run do -- Add parameter symbols for paramName in paramNames do let paramSymbol := createParameterSymbol paramName proc.header.name.toPretty - m := m.insert s!"{proc.header.name.snd}::{paramName}" paramSymbol + m := m.insert (getIdent paramName proc.header.name.snd) paramSymbol -- Add local variable m := m.insert s!"{proc.header.name.snd}::1::z" zSymbol + m := m.insert s!"{proc.header.name.snd}::1::sum" sumSymbol + m := m.insert s!"{proc.header.name.snd}::1::count" countSymbol toString (toJson m) end Boogie diff --git a/Strata/Backends/CBMC/Common.lean b/Strata/Backends/CBMC/Common.lean index 1fc9bebdf..25f252502 100644 --- a/Strata/Backends/CBMC/Common.lean +++ b/Strata/Backends/CBMC/Common.lean @@ -230,6 +230,19 @@ def mkSymbol (identifier : String) (symbolType : Json) : Json := ]) ] +def createParameterSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol := + createSymbol baseName "1" true true s!"{functionName}::" functionName config + +def createLocalSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol := + let fullName := s!"{functionName}::1::{baseName}" + createSymbol baseName "5" false false s!"{functionName}::1::" functionName config fullName + +def getIdent (varName: String) (functionName: String) : String := + if varName == "x" ∨ varName == "y" then + s!"{functionName}::{varName}" + else + s!"{functionName}::1::{varName}" + ------------------------------------------------------------------------------- /-! # Constants -/ @@ -342,7 +355,7 @@ def mkParameter (baseName : String) (functionName : String) (line : String) (con ("id", "parameter"), ("namedSub", Json.mkObj [ ("#base_name", Json.mkObj [("id", baseName)]), - ("#identifier", Json.mkObj [("id", s!"{functionName}::{baseName}")]), + ("#identifier", Json.mkObj [("id", (getIdent baseName functionName))]), ("#source_location", mkSourceLocation config.sourceFile functionName line config), ("type", mkIntType config) ]) @@ -429,7 +442,9 @@ def opToStr (op: String) : String := | "Int.Le" => "<=" | "Int.Add" => "+" | "Int.Sub" => "-" - | _ => panic! "Unimplemented" + | "Bool.And" => "&&" + | "Bool.Or" => "||" + | _ => panic! s!"Unimplemented: {op}" def opToOutTypeJson (op: String) (config : CBMCConfig := .empty): Json := match op with @@ -439,7 +454,9 @@ def opToOutTypeJson (op: String) (config : CBMCConfig := .empty): Json := | "<=" => boolType | "+" => mkIntType config | "-" => mkIntType config - | _ => panic! "Unimplemented" + | "&&" => boolType + | "||" => boolType + | _ => panic! s!"Unimplemented: {op}" def mkBinaryOp (op : String) (line : String) (functionName : String) (left : Json) (right : Json) (config : CBMCConfig := .empty) : Json := @@ -452,13 +469,6 @@ def mkBinaryOp (op : String) (line : String) (functionName : String) (left : Jso ("sub", Json.arr #[left, right]) ] -def createParameterSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol := - createSymbol baseName "1" true true s!"{functionName}::" functionName config - -def createLocalSymbol (baseName : String) (functionName : String) (config : CBMCConfig := .empty) : CBMCSymbol := - let fullName := s!"{functionName}::1::{baseName}" - createSymbol baseName "5" false false s!"{functionName}::1::" functionName config fullName - ------------------------------------------------------------------------------- /-! # Code -/ diff --git a/Strata/Backends/CBMC/StrataToCBMC.lean b/Strata/Backends/CBMC/StrataToCBMC.lean index ffae7d1ff..aeb53db2d 100644 --- a/Strata/Backends/CBMC/StrataToCBMC.lean +++ b/Strata/Backends/CBMC/StrataToCBMC.lean @@ -50,20 +50,6 @@ def myFunc : Strata.C_Simp.Function := SimpleTestEnvAST.fst.funcs.head! def lexprToCBMC (expr : Strata.C_Simp.Expression.Expr) (functionName : String) : Json := let cfg := CBMCConfig.empty match expr with - | .app (.app (.op op _) (.fvar varName _)) (.const value _) => - mkBinaryOp (opToStr op) "2" functionName (config := cfg) - (Json.mkObj [ - ("id", "symbol"), - ("namedSub", Json.mkObj [ - ("#base_name", Json.mkObj [("id", varName)]), - ("#id_class", Json.mkObj [("id", "1")]), - ("#lvalue", Json.mkObj [("id", "1")]), - ("#source_location", mkSourceLocation "from_andrew.c" functionName "2" cfg), - ("identifier", Json.mkObj [("id", s!"{functionName}::{varName}")]), - ("type", mkIntType cfg) - ]) - ]) - (mkConstant value "10" (mkSourceLocation "from_andrew.c" functionName "2" cfg) cfg) | .const "true" _ => Json.mkObj [ ("id", "notequal"), @@ -82,7 +68,23 @@ def lexprToCBMC (expr : Strata.C_Simp.Expression.Expr) (functionName : String) : ] ]) ] - | _ => panic! "Unimplemented" + | (.const value _) => (mkConstant value "10" (mkSourceLocation "from_andrew.c" functionName "2" cfg) cfg) + | (.fvar varName _) => (Json.mkObj [ + ("id", "symbol"), + ("namedSub", Json.mkObj [ + ("#base_name", Json.mkObj [("id", varName)]), + ("#id_class", Json.mkObj [("id", "1")]), + ("#lvalue", Json.mkObj [("id", "1")]), + ("#source_location", mkSourceLocation "from_andrew.c" functionName "2" cfg), + ("identifier", Json.mkObj [("id", getIdent varName functionName)]), + ("type", mkIntType cfg) + ]) + ]) + | .app (.app (.op op _) lhs) rhs => + mkBinaryOp (opToStr op) "2" functionName (config := cfg) + (lexprToCBMC lhs functionName) + (lexprToCBMC rhs functionName) + | _ => panic! s!"Unimplemented {expr}" def createContractSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol := let cfg := CBMCConfig.empty @@ -196,11 +198,10 @@ def exprToJson (e : Strata.C_Simp.Expression.Expr) (loc: SourceLoc) : Json := match e with | .app (.app (.op op _) left) right => let leftJson := match left with - | .fvar "z" _ => mkLvalueSymbol s!"{loc.functionName}::1::z" loc.lineNum loc.functionName cfg - | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{varName}" loc.lineNum loc.functionName cfg + | .fvar varName _ => mkLvalueSymbol (getIdent varName loc.functionName) loc.lineNum loc.functionName cfg | _ => exprToJson left loc let rightJson := match right with - | .fvar varName _ => mkLvalueSymbol s!"{loc.functionName}::{varName}" loc.lineNum loc.functionName cfg + | .fvar varName _ => mkLvalueSymbol (getIdent varName loc.functionName) loc.lineNum loc.functionName cfg | .const value _ => mkConstant value "10" (mkSourceLocation "from_andrew.c" loc.functionName loc.lineNum cfg) cfg | _ => exprToJson right loc mkBinaryOp (opToStr op) loc.lineNum loc.functionName leftJson rightJson cfg @@ -319,6 +320,19 @@ partial def stmtToJson (e : Strata.C_Simp.Statement) (loc: SourceLoc) : Json := blockToJson elseb loc, ]) ] + | .loop guard _ _ body _ => + Json.mkObj [ + ("id", "code"), + ("namedSub", Json.mkObj [ + ("#source_location", mkSourceLocation "from_andrew.c" loc.functionName "8"), + ("statement", Json.mkObj [("id", "while")]), + ("type", emptyType) + ]), + ("sub", Json.arr #[ + exprToJson guard loc, + blockToJson body loc + ]) + ] | _ => panic! "Unimplemented" end @@ -382,6 +396,8 @@ def testSymbols (myFunc: Strata.C_Simp.Function) : String := Id.run do -- Hardcode local variable for now let zSymbol := createLocalSymbol "z" myFunc.name + let sumSymbol := createLocalSymbol "sum" myFunc.name + let countSymbol := createLocalSymbol "count" myFunc.name -- Build symbol map let mut m : Map String CBMCSymbol := Map.empty @@ -395,6 +411,8 @@ def testSymbols (myFunc: Strata.C_Simp.Function) : String := Id.run do -- Add local variable m := m.insert s!"{myFunc.name}::1::z" zSymbol + m := m.insert s!"{myFunc.name}::1::sum" sumSymbol + m := m.insert s!"{myFunc.name}::1::count" countSymbol toString (toJson m) diff --git a/Strata/Backends/CBMC/compare_cbmc_json.sh b/Strata/Backends/CBMC/compare_cbmc_json.sh index 5c61f7a42..1d9e9f874 100755 --- a/Strata/Backends/CBMC/compare_cbmc_json.sh +++ b/Strata/Backends/CBMC/compare_cbmc_json.sh @@ -2,8 +2,8 @@ # This is useful if e.g., you ask Claude to refactor your code and want it to test the refactoring doesn't change the test file. -lake exe StrataToCBMC Strata/Backends/CBMC/tests/simpleTest.csimp.st > foo.json +lake exe StrataToCBMC Strata/Backends/CBMC/tests/testLoop.csimp.st > foo.json python3 Strata/Backends/CBMC/resources/process_json.py combine Strata/Backends/CBMC/resources/defaults.json foo.json > full.json -python3 Strata/Backends/CBMC/resources/process_json.py compare StrataTest/Backends/CBMC/simple_test_goto.json full.json +python3 Strata/Backends/CBMC/resources/process_json.py compare StrataTest/Backends/CBMC/simple_test_loop_goto.json full.json rm foo.json full.json \ No newline at end of file diff --git a/Strata/Backends/CBMC/run_strata_cbmc.sh b/Strata/Backends/CBMC/run_strata_cbmc.sh index 1036db261..67cbab7c0 100755 --- a/Strata/Backends/CBMC/run_strata_cbmc.sh +++ b/Strata/Backends/CBMC/run_strata_cbmc.sh @@ -7,7 +7,11 @@ lake exe StrataToCBMC $1 > foo.json python3 Strata/Backends/CBMC/resources/process_json.py combine Strata/Backends/CBMC/resources/defaults.json foo.json > full.json $CBMC_DIR/symtab2gb full.json --out full.goto -$CBMC_DIR/goto-instrument --enforce-contract simpleTest full.goto full_checking.goto -$CBMC_DIR/cbmc full_checking.goto --function simpleTest --trace -rm foo.json full.json full.goto full_checking.goto \ No newline at end of file + +$CBMC_DIR/goto-harness --function simpleTest --harness-function-name harness --harness-type call-function full.goto b.out +$CBMC_DIR/goto-cc b.out --function harness -o c.out +$CBMC_DIR/goto-instrument --dfcc harness --enforce-contract simpleTest c.out d.out +$CBMC_DIR/cbmc d.out + +rm foo.json full.json full.goto b.out c.out d.out diff --git a/Strata/Backends/CBMC/tests/testLoop.boogie.st b/Strata/Backends/CBMC/tests/testLoop.boogie.st new file mode 100644 index 000000000..21b30468e --- /dev/null +++ b/Strata/Backends/CBMC/tests/testLoop.boogie.st @@ -0,0 +1,22 @@ +program Boogie; + +procedure simpleTest (x: int, y: int) returns (ret : int) +spec { +} +{ + assume [assume_pos]: (x > 0); + assume [assume_smol]: (x < 10); + var sum : int; + sum := 0; + var count : int; + count := 0; + while + (count < x) + invariant (sum == count * x); + { + count := count + 1; + sum := sum + x; + } + assert [assert_pos]: (sum > 0); + ret := sum; +}; \ No newline at end of file diff --git a/Strata/Backends/CBMC/tests/testLoop.c b/Strata/Backends/CBMC/tests/testLoop.c new file mode 100644 index 000000000..6d1e20bf0 --- /dev/null +++ b/Strata/Backends/CBMC/tests/testLoop.c @@ -0,0 +1,15 @@ +int simpleTest(int x) + __CPROVER_requires((x > 0) && (x < 10)) + __CPROVER_ensures(1) +{ + __CPROVER_assume(x > 0); + __CPROVER_assume(x < 10); + int sum = 0; + int count = 0; + while(count < 5) { + count++; + sum += x; + } + __CPROVER_assert(sum > 0, "sum_pos"); + return sum; +} \ No newline at end of file diff --git a/Strata/Backends/CBMC/tests/testLoop.csimp.st b/Strata/Backends/CBMC/tests/testLoop.csimp.st new file mode 100644 index 000000000..152723deb --- /dev/null +++ b/Strata/Backends/CBMC/tests/testLoop.csimp.st @@ -0,0 +1,23 @@ +program C_Simp; + +int procedure simpleTest (x: int, y: int) + //@pre ((x > 0) && (x < 10)); + //@post true; +{ + //@assume [assume_pos] (x > 0); + //@assume [assume_smol] (x < 10); + var sum : int; + sum = 0; + var count : int; + count = 0; + while + (count < x) + //@decreases (x-count) + //@invariant (count <= x && (sum == (count * x))) + { + count = count + 1; + sum = sum + x; + } + //@assert [assert_pos] (sum > 0); + return sum; +} \ No newline at end of file diff --git a/StrataTest/Backends/CBMC/simple_test_loop_goto.json b/StrataTest/Backends/CBMC/simple_test_loop_goto.json new file mode 100644 index 000000000..7acdd807d --- /dev/null +++ b/StrataTest/Backends/CBMC/simple_test_loop_goto.json @@ -0,0 +1,9301 @@ + { + "symbolTable": { + "simpleTest::1::count": { + "baseName": "count", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "simpleTest::1::count", + "prettyName": "simpleTest::1::count", + "prettyType": "signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + }, + "simpleTest::1::sum": { + "baseName": "sum", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "simpleTest::1::sum", + "prettyName": "simpleTest::1::sum", + "prettyType": "signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + }, + "__CPROVER_assume": { + "baseName": "__CPROVER_assume", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "", + "name": "__CPROVER_assume", + "prettyName": "__CPROVER_assume", + "prettyType": "void (__CPROVER_bool)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "assumption" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assume" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "simpleTest": { + "baseName": "simpleTest", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "simpleTest", + "prettyName": "simpleTest", + "prettyType": "signed int (signed int x)", + "prettyValue": "{\n __CPROVER_assume(x > 0);\n __CPROVER_assume(x < 10);\n signed int sum=0;\n signed int count=0;\n while(count < 5)\n {\n count++;\n sum += x;\n }\n __CPROVER_assert(sum > 0, \"sum_pos\");\n return sum;\n}", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "x" + }, + "#identifier": { + "id": "simpleTest::x" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#end_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_assume" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "assumption" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assume" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": ">", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_assume" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "assumption" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assume" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "<", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "A" + } + } + } + ] + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "decl" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::sum" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "decl" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::count" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "while" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "<", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::count" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "5" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#end_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "postincrement" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::count" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign+" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::sum" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "expression" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_assert" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "assertion" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assert" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + } + }, + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "description" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assert" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assert" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "8" + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": ">", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::sum" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "sum_pos" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + ] + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "return" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::1::sum" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + }, + "__CPROVER_architecture_NULL_is_zero": { + "baseName": "__CPROVER_architecture_NULL_is_zero", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_NULL_is_zero", + "prettyName": "__CPROVER_architecture_NULL_is_zero", + "prettyType": "integer", + "prettyValue": "(integer)1", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + ] + } + }, + "__CPROVER_architecture_endianness": { + "baseName": "__CPROVER_architecture_endianness", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_endianness", + "prettyName": "__CPROVER_architecture_endianness", + "prettyType": "integer", + "prettyValue": "(integer)1", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "17" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + ] + } + }, + "__CPROVER_architecture_memory_operand_size": { + "baseName": "__CPROVER_architecture_memory_operand_size", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_memory_operand_size", + "prettyName": "__CPROVER_architecture_memory_operand_size", + "prettyType": "integer", + "prettyValue": "(integer)4", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "4" + } + } + } + ] + } + }, + "__CPROVER_architecture_alignment": { + "baseName": "__CPROVER_architecture_alignment", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_alignment", + "prettyName": "__CPROVER_architecture_alignment", + "prettyType": "integer", + "prettyValue": "(integer)1", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "15" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + } + ] + } + }, + "__CPROVER_architecture_wchar_t_is_unsigned": { + "baseName": "__CPROVER_architecture_wchar_t_is_unsigned", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_wchar_t_is_unsigned", + "prettyName": "__CPROVER_architecture_wchar_t_is_unsigned", + "prettyType": "integer", + "prettyValue": "(integer)0", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "14" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER_architecture_char_is_unsigned": { + "baseName": "__CPROVER_architecture_char_is_unsigned", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_char_is_unsigned", + "prettyName": "__CPROVER_architecture_char_is_unsigned", + "prettyType": "integer", + "prettyValue": "(integer)0", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "13" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + }, + "__CPROVER__start::x": { + "baseName": "x", + "isAuxiliary": true, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "", + "name": "__CPROVER__start::x", + "prettyName": "", + "prettyType": "signed int", + "prettyValue": "", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_wchar_t_width": { + "baseName": "__CPROVER_architecture_wchar_t_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_wchar_t_width", + "prettyName": "__CPROVER_architecture_wchar_t_width", + "prettyType": "integer", + "prettyValue": "(integer)32", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + ] + } + }, + "return'": { + "baseName": "return'", + "isAuxiliary": true, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "return'", + "prettyName": "", + "prettyType": "signed int", + "prettyValue": "", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_long_double_width": { + "baseName": "__CPROVER_architecture_long_double_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_long_double_width", + "prettyName": "__CPROVER_architecture_long_double_width", + "prettyType": "integer", + "prettyValue": "(integer)64", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "11" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + ] + } + }, + "__CPROVER_architecture_double_width": { + "baseName": "__CPROVER_architecture_double_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_double_width", + "prettyName": "__CPROVER_architecture_double_width", + "prettyType": "integer", + "prettyValue": "(integer)64", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "10" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + ] + } + }, + "__CPROVER__start": { + "baseName": "__CPROVER__start", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "nil" + }, + "mode": "C", + "module": "", + "name": "__CPROVER__start", + "prettyName": "", + "prettyType": "void (void)", + "prettyValue": "{\n\n__CPROVER_HIDE:\n ;\n __CPROVER_initialize();\n signed int x;\n x = NONDET(signed int);\n INPUT(\"x\", x);\n return'=simpleTest(x);\n OUTPUT(\"return'\", return');\n}", + "type": { + "id": "code", + "namedSub": { + "parameters": { + "id": "" + }, + "return_type": { + "id": "empty" + } + } + }, + "value": { + "id": "code", + "namedSub": { + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "label": { + "id": "__CPROVER_HIDE" + }, + "statement": { + "id": "label" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "skip" + }, + "type": { + "id": "empty" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "nil" + }, + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_initialize" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + } + } + }, + { + "id": "arguments" + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "decl" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER__start::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER__start::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "side_effect", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "is_nondet_nullable": { + "id": "1" + }, + "statement": { + "id": "nondet" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "input" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "2" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "x" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER__start::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "function_call" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "return'" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest" + }, + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "x" + }, + "#identifier": { + "id": "simpleTest::x" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + } + }, + { + "id": "arguments", + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER__start::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "output" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "return'" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + }, + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "return'" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + } + ] + } + }, + "__CPROVER_architecture_single_width": { + "baseName": "__CPROVER_architecture_single_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_single_width", + "prettyName": "__CPROVER_architecture_single_width", + "prettyType": "integer", + "prettyValue": "(integer)32", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + ] + } + }, + "__CPROVER_architecture_pointer_width": { + "baseName": "__CPROVER_architecture_pointer_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_pointer_width", + "prettyName": "__CPROVER_architecture_pointer_width", + "prettyType": "integer", + "prettyValue": "(integer)64", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + ] + } + }, + "__CPROVER_architecture_short_int_width": { + "baseName": "__CPROVER_architecture_short_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_short_int_width", + "prettyName": "__CPROVER_architecture_short_int_width", + "prettyType": "integer", + "prettyValue": "(integer)16", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "10" + } + } + } + ] + } + }, + "__CPROVER_architecture_bool_width": { + "baseName": "__CPROVER_architecture_bool_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_bool_width", + "prettyName": "__CPROVER_architecture_bool_width", + "prettyType": "integer", + "prettyValue": "(integer)8", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "4" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "8" + } + } + } + ] + } + }, + "__CPROVER_architecture_word_size": { + "baseName": "__CPROVER_architecture_word_size", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_word_size", + "prettyName": "__CPROVER_architecture_word_size", + "prettyType": "integer", + "prettyValue": "(integer)32", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + ] + } + }, + "__CPROVER_memory_leak": { + "baseName": "__CPROVER_memory_leak", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_memory_leak", + "prettyName": "__CPROVER_memory_leak", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "__CPROVER_architecture_int_width": { + "baseName": "__CPROVER_architecture_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_int_width", + "prettyName": "__CPROVER_architecture_int_width", + "prettyType": "integer", + "prettyValue": "(integer)32", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "20" + } + } + } + ] + } + }, + "__CPROVER_is_freeable": { + "baseName": "__CPROVER_is_freeable", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "34" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_is_freeable", + "prettyName": "__CPROVER_is_freeable", + "prettyType": "__CPROVER_bool (void *)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "34" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_is_freeable" + }, + "line": { + "id": "34" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_is_freeable" + }, + "line": { + "id": "34" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "34" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "bool" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_max_malloc_size": { + "baseName": "__CPROVER_max_malloc_size", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_max_malloc_size", + "prettyName": "__CPROVER_max_malloc_size", + "prettyType": "__CPROVER_size_t", + "prettyValue": "36028797018963968ul", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "80000000000000" + } + } + } + }, + "__CPROVER_architecture_long_long_int_width": { + "baseName": "__CPROVER_architecture_long_long_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_long_long_int_width", + "prettyName": "__CPROVER_architecture_long_long_int_width", + "prettyType": "integer", + "prettyValue": "(integer)64", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + ] + } + }, + "__CPROVER_assert": { + "baseName": "__CPROVER_assert", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "", + "name": "__CPROVER_assert", + "prettyName": "__CPROVER_assert", + "prettyType": "void (__CPROVER_bool, const char *)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "assertion" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assert" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + } + }, + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "description" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assert" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assert" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "8" + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "20" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_freeable": { + "baseName": "__CPROVER_freeable", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_freeable", + "prettyName": "__CPROVER_freeable", + "prettyType": "void (void *)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_freeable" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_freeable" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "33" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_long_int_width": { + "baseName": "__CPROVER_architecture_long_int_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_long_int_width", + "prettyName": "__CPROVER_architecture_long_int_width", + "prettyType": "integer", + "prettyValue": "(integer)64", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "40" + } + } + } + ] + } + }, + "__CPROVER_object_from": { + "baseName": "__CPROVER_object_from", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "31" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_object_from", + "prettyName": "__CPROVER_object_from", + "prettyType": "void (void *)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "31" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_from" + }, + "line": { + "id": "31" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_from" + }, + "line": { + "id": "31" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "31" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "31" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "simpleTest::x": { + "baseName": "x", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": true, + "isProperty": false, + "isStateVar": true, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "simpleTest::x", + "prettyName": "", + "prettyType": "signed int", + "prettyValue": "", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_object_upto": { + "baseName": "__CPROVER_object_upto", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "29" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_object_upto", + "prettyName": "__CPROVER_object_upto", + "prettyType": "void (void *, __CPROVER_size_t)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "29" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_upto" + }, + "line": { + "id": "29" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_upto" + }, + "line": { + "id": "29" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "29" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + }, + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "size" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_upto" + }, + "line": { + "id": "30" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "29" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_os": { + "baseName": "__CPROVER_architecture_os", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "19" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_os", + "prettyName": "__CPROVER_architecture_os", + "prettyType": "const char *", + "prettyValue": "\"macos\"", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "19" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "19" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "6" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "macos" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + }, + "__CPROVER_assignable": { + "baseName": "__CPROVER_assignable", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "26" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_assignable", + "prettyName": "__CPROVER_assignable", + "prettyType": "void (void *, __CPROVER_size_t, __CPROVER_bool)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "26" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assignable" + }, + "line": { + "id": "26" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assignable" + }, + "line": { + "id": "26" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "26" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + }, + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "size" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assignable" + }, + "line": { + "id": "27" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + } + } + }, + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "is_ptr_to_ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_assignable" + }, + "line": { + "id": "28" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "26" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_constant_infinity_uint": { + "baseName": "__CPROVER_constant_infinity_uint", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_constant_infinity_uint", + "prettyName": "__CPROVER_constant_infinity_uint", + "prettyType": "const unsigned int", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_int" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_architecture_arch": { + "baseName": "__CPROVER_architecture_arch", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_arch", + "prettyName": "__CPROVER_architecture_arch", + "prettyType": "const char *", + "prettyValue": "\"arm64\"", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "#constant": { + "id": "1" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "address_of", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + } + }, + "sub": [ + { + "id": "index", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + }, + "sub": [ + { + "id": "string_constant", + "namedSub": { + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "18" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "array", + "namedSub": { + "size": { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "6" + } + } + } + }, + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "arm64" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + }, + "__CPROVER_initialize": { + "baseName": "__CPROVER_initialize", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_initialize", + "prettyName": "__CPROVER_initialize", + "prettyType": "void (void)", + "prettyValue": "{\n\n__CPROVER_HIDE:\n ;\n __CPROVER_dead_object = NULL;\n __CPROVER_deallocated = NULL;\n __CPROVER_max_malloc_size = 36028797018963968ul;\n __CPROVER_memory_leak = NULL;\n __CPROVER_rounding_mode = 0;\n}", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "" + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "24" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "block" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "label": { + "id": "__CPROVER_HIDE" + }, + "statement": { + "id": "label" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "code", + "namedSub": { + "statement": { + "id": "skip" + }, + "type": { + "id": "empty" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_dead_object" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_deallocated" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_max_malloc_size" + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "12" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "80000000000000" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_memory_leak" + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "9" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + ] + }, + { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "statement": { + "id": "assign" + }, + "type": { + "id": "empty" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "__CPROVER_rounding_mode" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + }, + "__CPROVER_architecture_char_width": { + "baseName": "__CPROVER_architecture_char_width", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_architecture_char_width", + "prettyName": "__CPROVER_architecture_char_width", + "prettyType": "integer", + "prettyValue": "(integer)8", + "type": { + "id": "integer" + }, + "value": { + "id": "typecast", + "namedSub": { + "type": { + "id": "integer" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "5" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "8" + } + } + } + ] + } + }, + "__CPROVER_object_whole": { + "baseName": "__CPROVER_object_whole", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "32" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_object_whole", + "prettyName": "__CPROVER_object_whole", + "prettyType": "void (void *)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "32" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_whole" + }, + "line": { + "id": "32" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_object_whole" + }, + "line": { + "id": "32" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "32" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "32" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_dead_object": { + "baseName": "__CPROVER_dead_object", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_dead_object", + "prettyName": "__CPROVER_dead_object", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "8" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "__CPROVER_deallocated": { + "baseName": "__CPROVER_deallocated", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_deallocated", + "prettyName": "__CPROVER_deallocated", + "prettyType": "const void *", + "prettyValue": "NULL", + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "constant", + "namedSub": { + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#constant": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "7" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + }, + "value": { + "id": "NULL" + } + } + } + }, + "contract::simpleTest": { + "baseName": "simpleTest", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": false, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": true, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "contract::simpleTest", + "prettyName": "simpleTest", + "prettyType": "signed int (signed int x)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#spec_assigns": { + "id": "" + }, + "#spec_ensures": { + "id": "", + "sub": [ + { + "id": "lambda", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "mathematical_function", + "sub": [ + { + "id": "", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + ] + }, + { + "id": "bool" + } + ] + } + }, + "sub": [ + { + "id": "tuple", + "namedSub": { + "type": { + "id": "tuple" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_return_value" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + { + "id": "notequal", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "3" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "1" + } + } + }, + { + "id": "constant", + "namedSub": { + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + } + ] + } + ] + }, + "#spec_frees": { + "id": "" + }, + "#spec_requires": { + "id": "", + "sub": [ + { + "id": "lambda", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "mathematical_function", + "sub": [ + { + "id": "", + "sub": [ + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + ] + }, + { + "id": "bool" + } + ] + } + }, + "sub": [ + { + "id": "tuple", + "namedSub": { + "type": { + "id": "tuple" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "__CPROVER_return_value" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "symbol", + "namedSub": { + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + { + "id": "and", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": ">", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#base_name": { + "id": "x" + }, + "#id_class": { + "id": "1" + }, + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + ] + }, + { + "id": "<", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "bool" + } + }, + "sub": [ + { + "id": "symbol", + "namedSub": { + "#base_name": { + "id": "x" + }, + "#id_class": { + "id": "1" + }, + "#lvalue": { + "id": "1" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "identifier": { + "id": "simpleTest::x" + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "2" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "A" + } + } + } + ] + } + ] + } + ] + } + ] + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "x" + }, + "#identifier": { + "id": "simpleTest::x" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "Strata/Backends/CBMC/tests/testLoop.c" + }, + "function": { + "id": "simpleTest" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + } + ] + }, + "return_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_memory": { + "baseName": "__CPROVER_memory", + "isAuxiliary": false, + "isExported": false, + "isExtern": true, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_memory", + "prettyName": "__CPROVER_memory", + "prettyType": "unsigned char [INFINITY()]", + "prettyValue": "", + "type": { + "id": "array", + "namedSub": { + "#index_type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "size": { + "id": "infinity", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "6" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_long_int" + }, + "width": { + "id": "64" + } + } + } + } + } + }, + "sub": [ + { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_char" + }, + "width": { + "id": "8" + } + } + } + ] + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_size_t": { + "baseName": "__CPROVER_size_t", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": true, + "isInput": false, + "isLvalue": false, + "isMacro": true, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": true, + "isType": true, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_size_t", + "prettyName": "__CPROVER_size_t", + "prettyType": "__CPROVER_size_t", + "prettyValue": "", + "type": { + "id": "unsignedbv", + "namedSub": { + "#c_type": { + "id": "unsigned_long_int" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "line": { + "id": "1" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "#typedef": { + "id": "__CPROVER_size_t" + }, + "width": { + "id": "64" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_was_freed": { + "baseName": "__CPROVER_was_freed", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": false, + "isThreadLocal": false, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_was_freed", + "prettyName": "__CPROVER_was_freed", + "prettyType": "__CPROVER_bool (void *)", + "prettyValue": "", + "type": { + "id": "code", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "parameters": { + "id": "", + "sub": [ + { + "id": "parameter", + "namedSub": { + "#base_name": { + "id": "ptr" + }, + "#identifier": { + "id": "" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_was_freed" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "pointer", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "__CPROVER_was_freed" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "width": { + "id": "64" + } + }, + "sub": [ + { + "id": "empty", + "namedSub": { + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "35" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + } + } + } + ] + } + } + } + ] + }, + "return_type": { + "id": "bool" + } + } + }, + "value": { + "id": "nil" + } + }, + "__CPROVER_rounding_mode": { + "baseName": "__CPROVER_rounding_mode", + "isAuxiliary": false, + "isExported": false, + "isExtern": false, + "isFileLocal": false, + "isInput": false, + "isLvalue": true, + "isMacro": false, + "isOutput": false, + "isParameter": false, + "isProperty": false, + "isStateVar": false, + "isStaticLifetime": true, + "isThreadLocal": true, + "isType": false, + "isVolatile": false, + "isWeak": false, + "location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "mode": "C", + "module": "testLoop", + "name": "__CPROVER_rounding_mode", + "prettyName": "__CPROVER_rounding_mode", + "prettyType": "signed int", + "prettyValue": "0", + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "constant", + "namedSub": { + "#base": { + "id": "10" + }, + "#source_location": { + "id": "", + "namedSub": { + "file": { + "id": "" + }, + "function": { + "id": "" + }, + "line": { + "id": "16" + }, + "working_directory": { + "id": "/Users/anmwells/Development/Strata" + } + } + }, + "type": { + "id": "signedbv", + "namedSub": { + "#c_type": { + "id": "signed_int" + }, + "width": { + "id": "32" + } + } + }, + "value": { + "id": "0" + } + } + } + } + } + }