[depends: #1339] Get goto model by kroening · Pull Request #1285 · diffblue/cbmc

kroening · 2017-08-23T10:33:57Z

This is a new and simpler way to arrive at a goto program.

tautschnig · 2017-08-23T10:42:51Z

src/goto-programs/goto_convert_functions.h

Is this comment still true?

tautschnig · 2017-08-23T10:44:48Z

src/goto-programs/get_goto_model.cpp

How is the actual error going to be conveyed?

Message handler!

tautschnig · 2017-08-23T10:52:56Z

src/goto-programs/get_goto_model.cpp

How is this not leaking memory?

tautschnig · 2017-08-23T10:54:25Z

src/goto-programs/get_goto_model.cpp

Shouldn't this also do

source_locationt location; location.set_file(filename); message.error().source_location=location;

as is done above?

Contemplated it, but then we'd be sending out filenames that we know don't exist.

peterschrammel · 2017-08-23T10:35:46Z

src/goto-programs/get_goto_model.cpp

no space after &

peterschrammel · 2017-08-23T15:08:05Z

src/cbmc/cbmc_parse_options.cpp

get_message_handler() ?

peterschrammel · 2017-08-23T15:09:08Z

src/cbmc/cbmc_parse_options.cpp

get_message_handler() ?

peterschrammel · 2017-08-23T15:09:37Z

src/cbmc/cbmc_parse_options.cpp

get_message_handler() ?

peterschrammel · 2017-08-23T15:10:14Z

src/cbmc/cbmc_parse_options.cpp

get_message_handler() ?

tautschnig · 2017-08-25T17:29:21Z

The failing CI tests indicate that there is work left to be done.

kroening · 2017-09-03T22:11:32Z

#1339 prepares this.

thomasspriggs · 2021-02-23T10:47:29Z

I am going to close this PR as it appears that work on it has been inactive for an extended period of time. This is not any judgement on how worthwhile this work is. This is part of an effort to reduce the number of open PRs which are not being actively worked on. If you still think it would be worthwhile to get this merged then the branch should be re-based on the latest version of develop and the PR re-opened.

kroening force-pushed the get-goto-model branch 2 times, most recently from ad06057 to 3b3ab2b Compare August 23, 2017 10:54

tautschnig reviewed Aug 23, 2017

View reviewed changes

kroening force-pushed the get-goto-model branch 8 times, most recently from a757b6f to e95796f Compare August 23, 2017 14:02

peterschrammel reviewed Aug 23, 2017

View reviewed changes

kroening force-pushed the get-goto-model branch 4 times, most recently from faf2d0f to 33fe5fd Compare August 24, 2017 16:41

kroening added 7 commits August 25, 2017 15:29

simplify API of goto_convert

f5dfcf2

added get_goto_model

de501bd

use get_goto_model in CBMC

11d4341

remove initialize_goto_model

9126f87

brief list of symbols, from language_uit

fac6d26

remove spurious references to langapi/language_ui.h

f212624

the main_class is now remembered in the symbol table

dd1ee91

kroening force-pushed the get-goto-model branch from 33fe5fd to dd1ee91 Compare August 25, 2017 14:42

kroening force-pushed the get-goto-model branch 3 times, most recently from 2866ca0 to dd1ee91 Compare August 29, 2017 11:28

kroening added the cleanup label Aug 29, 2017

tautschnig assigned kroening Sep 1, 2017

tautschnig changed the title ~~Get goto model~~ [depends: #1339] Get goto model Sep 4, 2017

thomasspriggs closed this Feb 23, 2021

Conversation

kroening commented Aug 23, 2017

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tautschnig commented Aug 25, 2017

Uh oh!

kroening commented Sep 3, 2017

Uh oh!

thomasspriggs commented Feb 23, 2021

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants