Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/kernel/byterun/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 1 kB image not shown  

Quelle  rocq_fix_code.h   Sprache: C

 
/***********************************************************************/
/*                                                                     */
/*                          Rocq Compiler                              */
/*                                                                     */
/*        Benjamin Gregoire, projets Logical and Cristal               */
/*                        INRIA Rocquencourt                           */
/*                                                                     */
/*                                                                     */
/***********************************************************************/


#ifndef _ROCQ_FIX_CODE_
#define _ROCQ_FIX_CODE_

#include <caml/mlvalues.h>
void * rocq_stat_alloc (asize_t sz);

#ifdef THREADED_CODE
void rocq_init_thread_code(void ** instr_table, void * instr_base);
#endif /*  THREADED_CODE */

extern code_t accumulate;

int rocq_is_instruction(opcode_t, opcode_t);
value rocq_tcode_of_code(value code);
value rocq_accumulate(value);
value rocq_makeaccu (value i);
value rocq_pushpop (value i);
value rocq_accucond (value i);

#endif /* _ROCQ_FIX_CODE_ */

100%


¤ Dauer der Verarbeitung: 0.10 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.