| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
|
| |
This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case.
For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
|
|
|
|
|
|
|
|
|
|
|
| |
- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.
|
|
|
|
|
|
| |
Now "expected at least %d" instead of "expected %d". Also improved
error message for __builtin_debug.
Bug 19872
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
Removed duplicated of, changed string to string literal for
wording than the C standard.
Bug 18004
|
| |
|
|\ |
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
The test is extended for integer constants smaller than 0. Also the
default constant used for the error is no longer 0 since this is
not a positive number.
Bug 19629
|
|/
|
|
|
|
|
|
|
|
| |
Now each warning either has a name and can be turned on/off, made
into an error,etc. or is a warning that always will be triggered.
The message of the warnings are similar to the ones emited by
gcc/clang and all fit into one line.
Furthermore the diagnostics are now colored if colored output is
available.
Bug 18004
|
|
|
|
|
|
|
|
| |
Most of the code can be String.uppercase usages can either be
replaced by a more specialized version of coqstring_of_camlstring
(which is also slightly more effecient) or by specialized checks
that reject wrong code earlier.
Bug 19187
|
|\ |
|
| |
| |
| |
| | |
Also: in Events, use Senv.equiv to state invariance wrt changes of global envs.
|
| |
| |
| |
| |
| |
| | |
The functions for naming string and wstring literals no longer need
an env.
Bug 18394
|
| |
| |
| |
| |
| |
| | |
The code was mostly there for documentation effort. So warning
27 is deactivated again.
Bug 18349
|
| |
| |
| |
| | |
This reverts commit bac2a0854ea51217690bc6f225da62053ed7ac06.
|
| |
| |
| |
| |
| |
| | |
The ofs parameter is no longer used. Adopted the proofs and ml
code using it.
Bug 18394
|
|/
|
|
|
|
| |
Removed some unused variables, functions etc. and resolved some
problems which occur if all warnings except 3,4,9 and 29 are active.
Bug 18394.
|
|
|
|
|
|
| |
- Rename '-fstruct-return' into '-fstruct-passing', because this emulation affects both function result passing and function argument passing. Keep '-fstruct-return' as a deprecated synonymous for '-fstruct-passing'
- Remove the ability to change the ABI for struct passing via the '-fstruct-passing=<abi>' and '-fstruct-return=<abi>' command-line flags. This was more confusing than useful.
- Produce an error if a struct/union is passed as function argument and '-fstruct-passing' is not set. This used to be supported, using CompCert's default ABI for passing struct arguments. However, this default ABI does not match any of the standard ABIs of our target platforms, so it is better to reject than to silently produce ABI-incompatible code.
|
|
|
|
| |
Use tail-recursive operations to implement transformations on initializers for global arrays. This way, very large static initializers no longer cause stack overflows at compile-time.
|
|
|
|
|
|
| |
We should not remove any debug stmt inside of the cases. We should
just not warn in the case that init is only debugcalls.
Bug 17850
|
|
|
|
|
|
|
| |
Debug statements introduced during the translation result in warnings
when they are introduced at the head of the switch. Since they are
not used and the warning is not necessary we can remove them before.
Fix 17580.
|
|\
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Conflicts:
arm/TargetPrinter.ml
backend/CMparser.mly
backend/SelectLongproof.v
backend/Selectionproof.v
cfrontend/C2C.ml
checklink/Asm_printers.ml
checklink/Check.ml
checklink/Fuzz.ml
common/AST.v
debug/DebugInformation.ml
debug/DebugInit.ml
debug/DwarfPrinter.ml
debug/DwarfTypes.mli
debug/Dwarfgen.ml
exportclight/ExportClight.ml
ia32/TargetPrinter.ml
powerpc/Asm.v
powerpc/SelectOpproof.v
powerpc/TargetPrinter.ml
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
Instead of defining two functions for adding the mapping from atom
to debug id we use one function which then sets the corresponding
values.
Bug 17392.
|
| | |
|
|/
|
|
|
|
|
|
|
|
| |
The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example:
* in $ARCH/Machregs.v to define the register conventions for builtin functions;
* in the VST program logic from Princeton to treat thread primitives specially.
So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq.
This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.
|
|
|
|
| |
the code more robust and added indentation for convertCompositeDef
|
|
|
|
| |
scopes before the last statement.
|
|\
| |
| |
| |
| |
| | |
Conflicts:
debug/CtoDwarf.ml
debug/DwarfPrinter.ml
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
C2C: the code that insert debug builtins with the line numbers is now
in Unblock. Handle calls to __builtin_debug.
Unblock: generate __builtin_debug(1) for line numbers, carrying
the list of active scopes as extra arguments.
Generate __builtin_debug(6) for local variable declarations,
carrying the corresponding scope number as extra argument.
Constprop: avoid duplicating debug arguments that are constants already.
PrintAsmaux: show this extra debug info as comments.
|
| |
| |
| |
| |
| |
| | |
Scopes will be handled by a stack of all open scopes. This stack
then can also be used to generate the debug directives to track the
scopes through the rest of the passes.
|
| |
| |
| |
| |
| | |
Introduced a new dwarf generation from the information collected in
the DebugInformation and removed the old CtODwarf translation.
|
| |
| |
| |
| |
| |
| | |
Added functions to add more information to the debuging interface,
like the struct layout with offsets, bitifiled layout and removed
the no longer needed mapping from stamp to atom.
|
|\|
| |
| |
| | |
Merge branch 'master' into debug_locations
|
| |
| |
| |
| |
| |
| |
| |
| | |
Use EF_debug instead of EF_annot for line number annotations.
Introduce PrintAsmaux.print_debug_info (very incomplete).
powerpc/Asmexpand: revise expand_memcpy_small.
|
|/ |
|
|
|
|
|
|
|
|
|
| |
literals.
This is a follow-up to commit 350354c.
- Move Float.build_from_parsed to Fappli_IEEE_extra.Bparse
- Add early checks for overflow and underflow and prove them correct.
- Improve speed of Bparse by using a fast exponentiation (square-and-multiply).
|
| |
|
|
|
|
| |
an switch to bail out on earlier on unstructured switch.
|
|
|
|
|
|
| |
"old-style" unprototyped.
Use this info in printing function types for Csyntax and Clight.
|
|
|
|
|
|
|
|
|
|
|
|
| |
Ctyping: define a typechecker for whole programs.
Csyntax: introduce the type "pre-program" (non-dependent).
C2C: use Ctyping.econdition instead of Ctyping.econdition'.
Note: Ctyping.typecheck_program could be used as the first step
in the verified compilation pipeline. Then, retyping would
no longer be performed in C2C. We keep it this way (for the time
being) because retyping errors are reported more precisely in C2C than
in Ctyping.
|
|
|
|
|
|
|
|
|
|
| |
- Treat clobbered registers as being destroyed by EF_inline_asm builtins
(which is the truth, semantically).
- To enable the above, represent clobbers as Coq strings rather than idents
and move register_by_name from Machregsaux.ml to Machregs.v.
- Side benefit: more efficient implementation of Machregsaux.name_of_register.
-# Please enter the commit message for your changes. Lines starting
|
|
|
|
|
|
| |
(underflow).
Also: spurious '\n' in C2C.warning.
|
| |
|
|
|
|
|
|
|
|
| |
- support "r", "m" and "i" constraints
- support "%Q" and "%R" modifiers for register pairs
- support register clobbers
- split off analysis and transformation of asm statements in
cparser/ExtendedAsm.ml
|
| |
|
|\
| |
| | |
Extended annotations
|