diff options
| author | Guillaume Melquiond | 2020-08-30 09:05:39 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-11-13 15:13:23 +0100 |
| commit | fdd16113a042170022dce276e53e7a3308c0451c (patch) | |
| tree | 5a9972375ade00812092b648826e33e7b7b90d8a /kernel/byterun | |
| parent | 930e51c23f5a8778af02f7a971a404860d713346 (diff) | |
Remove unchecked arithmetic operations from VM, as they are not used.
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 18 |
2 files changed, 0 insertions, 20 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 9118410549..cd431dbf2e 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,8 +43,6 @@ void init_arity () { arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= - arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]= - arity[LTFLOAT]=arity[LEFLOAT]= arity[ISINT]=arity[AREINT2]=0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 3bee36b667..74eb4973d0 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1271,11 +1271,8 @@ value coq_interprete Instruct(CHECKADDINT63){ print_instr("CHECKADDINT63"); CheckInt2(); - } - Instruct(ADDINT63) { /* Adds the integer in the accumulator with the one ontop of the stack (which is poped)*/ - print_instr("ADDINT63"); Uint63_add(accu, *sp++); Next; } @@ -1309,9 +1306,6 @@ value coq_interprete Instruct (CHECKSUBINT63) { print_instr("CHECKSUBINT63"); CheckInt2(); - } - Instruct (SUBINT63) { - print_instr("SUBINT63"); /* returns the subtraction */ Uint63_sub(accu, *sp++); Next; @@ -1517,9 +1511,6 @@ value coq_interprete Instruct (CHECKLTINT63) { print_instr("CHECKLTINT63"); CheckInt2(); - } - Instruct (LTINT63) { - print_instr("LTINT63"); int b; Uint63_lt(b,accu,*sp++); accu = b ? coq_true : coq_false; @@ -1529,9 +1520,6 @@ value coq_interprete Instruct (CHECKLEINT63) { print_instr("CHECKLEINT63"); CheckInt2(); - } - Instruct (LEINT63) { - print_instr("LEINT63"); int b; Uint63_leq(b,accu,*sp++); accu = b ? coq_true : coq_false; @@ -1608,9 +1596,6 @@ value coq_interprete Instruct (CHECKLTFLOAT) { print_instr("CHECKLTFLOAT"); CheckFloat2(); - } - Instruct (LTFLOAT) { - print_instr("LTFLOAT"); accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; Next; } @@ -1618,9 +1603,6 @@ value coq_interprete Instruct (CHECKLEFLOAT) { print_instr("CHECKLEFLOAT"); CheckFloat2(); - } - Instruct (LEFLOAT) { - print_instr("LEFLOAT"); accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false; Next; } |