goto-gcc options parsing and new goto-cc specific options for large-scale builds #81
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
from
729a374 to
54f5a3f
Compare
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
from
54f5a3f to
096c909
Compare
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
from
096c909 to
f793e49
Compare
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
4 times, most recently
from
5c78066 to
94818e2
Compare
tautschnig
changed the title
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
2 times, most recently
from
27de9cc to
8486a20
Compare
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
from
8486a20 to
56ea228
Compare
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
from
56ea228 to
a708d80
Compare
Places the preprocessed (if applicable) source code in outfile in case parsing or type checking fails. This will speed up debugging when using goto-(g)cc in large-scale projects.
Also simplified version output logic.
The preprocessed source is appended to the assembler output produced by the compiler (if in hybrid mode). The section is delimited by ;; GOTO-CC or ## GOTO-CC, depending on the comment characters used by the target assembler. Each preprocessed line is prefixed by ;;/##. Such a source can then be used by goto-as (next commit).
GCC -combine emits the compiled code of multiple source files into one assembler output file.
…case Previously, any new non-gcc option (such as verbosity, native-compiler, etc required handling this option in more than one place). This is no longer necessary and instead testing for them via cmdline.get_value/cmdline.isset suffices.
This is used by newlib.
tautschnig
force-pushed
the
goto-gcc_native-compiler-linker
branch
from
a708d80 to
dddab58
Compare
|
@kroening Is there any chance of getting this pull request reviewed (and, ideally, merged) some time soon? I very much appreciate the work started in the branch gcc-style-errors, but that may both result in duplicate work as well as numerous conflicts. Thanks! |
smowton
pushed a commit
to smowton/cbmc
that referenced
this pull request
May 9, 2018
…espaces Added taint namespaces
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is just one additional patch over #36.