Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/output/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 2 kB image not shown  

Quellcode-Bibliothek ltac2_printf.out   Sprache: unbekannt

 
Columbo aufrufen.out Download desUnknown {[0] [0] [0]}Datei anzeigen

File "./output/ltac2_printf.v", line 5, characters 6-29:
Warning: Unused variable: x. [ltac2-unused-variable,ltac2,default]
42
- : unit = ()
abc
- : unit = ()
Foo
- : unit = ()
(1 + 1 = 0)
- : unit = ()
%
- : unit = ()
dummy
- : unit = ()
dummy
- : unit = ()
hello world!
- : unit = ()
ok foodummy bar yes
- : unit = ()
ok foodummy bar yes
- : unit = ()
ok foodummy bar yes
- : unit = ()
ok foodummy bar yes
- : unit = ()
File "./output/ltac2_printf.v", line 31, characters 28-33:
The command has indeed failed with message:
This expression has type string but an expression was expected of type 
int
File "./output/ltac2_printf.v", line 32, characters 28-29:
The command has indeed failed with message:
This expression has type int but an expression was expected of type 
string
File "./output/ltac2_printf.v", line 33, characters 28-33:
The command has indeed failed with message:
This expression has type string but an expression was expected of type 
ident
File "./output/ltac2_printf.v", line 34, characters 28-33:
The command has indeed failed with message:
This expression has type string but an expression was expected of type 
constr
File "./output/ltac2_printf.v", line 35, characters 40-42:
The command has indeed failed with message:
This expression has type unit but an expression was expected of type 
message
File "./output/ltac2_printf.v", line 36, characters 38-40:
The command has indeed failed with message:
This expression has type unit but an expression was expected of type 
message
File "./output/ltac2_printf.v", line 37, characters 58-63:
The command has indeed failed with message:
This expression has type string but an expression was expected of type 
int
File "./output/ltac2_printf.v", line 38, characters 43-48:
The command has indeed failed with message:
This expression has type string but an expression was expected of type 
int
File "./output/ltac2_printf.v", line 39, characters 28-29:
The command has indeed failed with message:
This expression has type int but an expression was expected of type 
message
- : unit = ()
- : unit = ()
- : unit = ()
File "./output/ltac2_printf.v", line 60, characters 0-81:
The command has indeed failed with message:
Uncaught Ltac2 exception: Assertion_failure
File "./output/ltac2_printf.v", line 61, characters 0-81:
The command has indeed failed with message:
Uncaught Ltac2 exception: Assertion_failure
- : string = ""
- : string = ""

[ 0.90Quellennavigators  ]