Hi Burkhart.

With cpp, I didn't realise this until a minute ago, but it can be set inside Isabelle.
Try something like 'declare [[cpp_path="foo"]]' before install_C_file. I guess you
could work further by pointing at a script that does the right thing on every
machine you care about?

With the array exception, it's pretty simple. The parser doesn't like arrays of unspecified
size. You can work around that by referencing InputField as a char ** rather than
a char *[]. We could probably have a lively debate as to whether the parser should
treat both of these as the same. Perhaps it should in this case, but that's not true for
every array/pointer geometry.

Cheers,
Thomas.

On 18/05/18 00:06, Burkhart Wolff wrote:

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
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel