#include <linux/kernel.h>
#include <linux/percpu.h>
#include <linux/avm_power.h>
#include <pmc_drv.h>

#define TEMPERATURE_SENSOR_INDEX 0u

/*@ logic integer fromCelsius( integer degrees ) = degrees * 10;
*/

/*@ requires \valid( value );
    assigns  *value;
    ensures (\result == -EIO) ||
            ((\result == 0) &&
            (fromCelsius(-21064) < *value < fromCelsius(21475)));
*/
static int cpu_temperature_callback(__maybe_unused void *handle,
				    __maybe_unused void *context, int *value)
{
	int temperature;

	if (GetCPUTemperature(&temperature) != kPMC_NO_ERROR)
		return -EIO;

        if ((temperature > 44091) || (temperature < (-43249)))
                return -EIO;


        /*@ assert rte: mem_access: \valid(value); */
        /*@ assert rte: signed_overflow: -2147483648 ≤ 48705 * temperature; */
        /*@ assert rte: signed_overflow: 48705 * temperature ≤ 2147483647; */
        /*@ assert rte: signed_overflow: 41004000 - (int)(48705 * temperature) ≤ 2147483647; */

	//copied from pvtmon_convert
	*value = (41004000 - 48705 * temperature) / 10000;
	return 0;
}

static int __init cpu_temperature_init(void)
{
	if (!TemperaturSensorRegister("CPU", cpu_temperature_callback,
				      TEMPERATURE_SENSOR_INDEX)) {
		pr_err("Could not register CPU Temperature sensor to AVM Power driver.\n");
	}
	return 0;
}

arch_initcall(cpu_temperature_init);