Dear all,
I stumbled into some problems with AutoCorres and would be grateful if someone could help me. I used the recent version autocorres1.4 under Isabelle2017.
A) Running under MacOS, cpp is apparently not running inside install_C_file (yes, I installed the cpp wrapper:
>>>>>>>>>>>>>>>>>>>>>> !/bin/bash
# Wrapper for clang C preprocessor on MacOS
export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre"
llvm-gcc -Wno-invalid-pp-token -E -x c $@
<<<<<<<<<<<<<<<<<<<<<<
and made sure that it is in the path of the shell in which I started Isabelle.)
Does anyone know a cause for this behaviour or a feasible workaround ? (besides doing the expansions by hand)
Is there an explicit Isabelle shell variable where the path to cpp must be set ?
B) I get a weird crash of AutoCorres without a clue what might cause it:
I have a T4.h file with >>>>>>>>>>>>>>>>>>>>>>>
#define N_TEETH ( 100 * MODULO ) // shaft encoder's number of teeth per turn #define SIZE_OF_SPEED_FIFO 10 // number of samples to compute average speed
extern const char *InputField[];
enum State { S1=1, S2, S3, S4, S5, S6, SFail=0 }; enum Status { FAIL, SUCCESS }; enum InputPatterns { Ph1 = 1, Ph2 = 5, Ph3 = 4, Ph4 = 6, Ph5 = 2, Ph6 = 3 };
struct OBits { int C1 ; int C2 ; int C3 ; } Obits;
/********* Output data *****************/ extern enum Status O_Position_Valid; extern unsigned int O_Position_Count; extern unsigned int Relative_Position; extern int Instantaneous_Speed; extern int Mean_Speed;
<<<<<<<<<<<<<<<<<<<<<<<<<<<<< and a T4.c file with:
>>>>>>>>>>>>>>>>>>>>>>>
#include "T4_AlgoODO.h"
enum Status O_P_V = SUCCESS; unsigned int O_P_C = 0; unsigned int Relative_Position = 0; int I_Speed = 0; int Mean_Speed = 0; int Acceleration = 0; int scale = 1000; int PI_approx = 3141; struct OBits Input; enum State OState; const unsigned int Radius = 500; const unsigned int Sampling_Rate = 400;
unsigned int F_O_P_C = 0; int Speed_FIFO[10 /*SIZE_OF_SPEED_FIFO*/];
int FIFO_pointer = 0; <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
Loading this in Isabelle/AutoCorres with:
>>>>>>>>>>>>>>>>>>>
install_C_file "code/c/T4.c” <<<<<<<<<<<<<<<<<<<<<<<<<
results in the following AutoCorres crash: … exception Fail raised (line 175 of "~/codebox/odo_new/odo/autocorres-1.4/c-parser/calculate_state.ML"): translate_inttype: incomplete array!
Can anybody tell me what this means and propose a workaround ?
Best regards
B. Wolff