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