diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 3bc8e548a1098d082cc30e5127ebc8675d30b2c7..d292539ff501de4c8b9f12103d3ee0dd60b00f3c 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -2119,7 +2119,8 @@ struct } let gotoChunk ~ghost (ln: string) (l: location) : chunk = - let gref = ref dummyStmt in + let dummy = {dummyStmt with labels = [Label (ln, l, false)]} in + let gref = ref dummy in addGoto ln gref; { stmts = [ mkStmt ~ghost ~valid_sid (Goto (gref, l)),[],[],[],[] ]; cases = []; diff --git a/tests/misc/issue-1337-goto-debug.i b/tests/misc/issue-1337-goto-debug.i new file mode 100644 index 0000000000000000000000000000000000000000..873ba45ff0db785d4eeb278f52023cd1ff10b267 --- /dev/null +++ b/tests/misc/issue-1337-goto-debug.i @@ -0,0 +1,12 @@ +/* run.config + OPT: -kernel-msg-key typing +*/ + +int x; + +void f() { + goto L; + x++; + L: x++; + return; +} diff --git a/tests/misc/oracle/issue-1337-goto-debug.res.oracle b/tests/misc/oracle/issue-1337-goto-debug.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..6decf15845665db24ff13ce5991d944744c1d326 --- /dev/null +++ b/tests/misc/oracle/issue-1337-goto-debug.res.oracle @@ -0,0 +1,213 @@ +[kernel] Parsing issue-1337-goto-debug.i (no preprocessing) +[kernel:typing:global] createGlobal: x +[kernel:typing:global] + makeGlobalVarinfo isadef=true vi.vname=x(20), vreferenced=false +[kernel:typing:global] x not in the env already +[kernel:typing:global] first definition for x(20) +[kernel:typing:global] Definition of f at issue-1337-goto-debug.i:7 +[kernel:typing:global] + makeGlobalVarinfo isadef=true vi.vname=f(21), vreferenced=false +[kernel:typing:global] f not in the env already +[kernel:typing:chunk] + Concat: + + + {} + WITH + + + {/*() <- + Calls: + + */ + goto L;} + LEADS TO + + + {/*() <- + Calls: + + */ + goto L;} +[kernel:typing:chunk] + Removing x from chunk + /* UNDEFINED ORDER */ + + + {} +[kernel:typing:cast] no cast to perform +[kernel:typing:cast] no cast to perform +[kernel:typing:cast] no cast to perform +[kernel:typing:chunk] + Concat: + + + {} + WITH + /* UNDEFINED ORDER */ + + + {/*() x <- + Calls: + + */ + x ++;} + LEADS TO + + + {/*() x <- + Calls: + + */ + x ++;} +[kernel:typing:chunk] + Concat: + + + {/*() <- + Calls: + + */ + goto L;} + WITH + + + {/*() x <- + Calls: + + */ + x ++;} + LEADS TO + + + {/*() <- + Calls: + + */ + goto L;; + /*() x <- + Calls: + + */ + x ++;} +[kernel:typing:chunk] + Removing x from chunk + /* UNDEFINED ORDER */ + + + {} +[kernel:typing:cast] no cast to perform +[kernel:typing:cast] no cast to perform +[kernel:typing:cast] no cast to perform +[kernel:typing:chunk] + Concat: + + + {} + WITH + /* UNDEFINED ORDER */ + + + {/*() x <- + Calls: + + */ + x ++;} + LEADS TO + + + {/*() x <- + Calls: + + */ + x ++;} +[kernel:typing:chunk] + Concat: + + + {/*() <- + Calls: + + */ + goto L;; + /*() x <- + Calls: + + */ + x ++;} + WITH + + + {/*() x <- + Calls: + + */ + L: x ++;} + LEADS TO + + + {/*() <- + Calls: + + */ + goto L;; + /*() x <- + Calls: + + */ + x ++;; + /*() x <- + Calls: + + */ + L: x ++;} +[kernel:typing:chunk] + Concat: + + + {/*() <- + Calls: + + */ + goto L;; + /*() x <- + Calls: + + */ + x ++;; + /*() x <- + Calls: + + */ + L: x ++;} + WITH + + + {/*() <- + Calls: + + */ + return;} + LEADS TO + + + {/*() <- + Calls: + + */ + goto L;; + /*() x <- + Calls: + + */ + x ++;; + /*() x <- + Calls: + + */ + L: x ++;; + /*() <- + Calls: + + */ + return;}